induction ts with
| nil => simp [MultiGeachConfluent];
| cons t ts ih =>
  simp;
  constructor;
  . exact definability_canonicalFrame_GeachAxiom (includeK := ⟨(Set.Subset.trans AxiomSet.MultiGeach.subsetK hAx)⟩) (by aesop)
  . apply ih;
    simp_all;
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
ts : List Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
hAx : 𝗚𝗲(ts) ⊆ Ax(L)
⊢ MultiGeachConfluent ts (CanonicalFrame L)
no goals