. exact definability_canonicalFrame_GeachAxiom (includeK := ⟨(Set.Subset.trans AxiomSet.MultiGeach.subsetK hAx)⟩) (by aesop)
case cons.left
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ GeachConfluent t (CanonicalFrame L)

case cons.right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ MultiGeachConfluent ts (CanonicalFrame L)
case cons.right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
inst✝ : Inhabited (MCT L)
t : Axioms.Geach.Taple
ts : List Axioms.Geach.Taple
ih : 𝗚𝗲(ts) ⊆ Ax(L) → MultiGeachConfluent ts (CanonicalFrame L)
hAx : 𝗚𝗲(t :: ts) ⊆ Ax(L)
⊢ MultiGeachConfluent ts (CanonicalFrame L)