Conj

lemma conj (ps : V) {s : V} (hs : IsFormulaSet L s)    (ds : ∀ i < len ps, Derivable T (insert ps.[i] s)) : Derivable T (insert (^⋀ ps) s) := by  have : ∀ k ≤ len ps, Derivable T (insert (^⋀ (takeLast ps k)) s) := by    intro k hk    induction k using ISigma1.sigma1_succ_induction    · definability    case zero => simpa using verum (by simp [hs]) (by simp)    case succ k ih =>      have ih : Derivable T (insert (^⋀ takeLast ps k) s) := ih (le_trans le_self_add hk)      have : Derivable T (insert ps.[len ps - (k + 1)] s) := ds (len ps - (k + 1)) ((tsub_lt_iff_left hk).mpr (by simp))      simpa [takeLast_succ_of_lt (succ_le_iff_lt.mp hk)] using this.and ih  simpa using this (len ps) (by rfl)