assumption
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ a ∈ bs
no goals