tauto
case left.inl
α : Type u_1
Ax : AxiomSet α
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 : b ∈ bs → as ⊆ bs → 𝗴𝗲(b) ⊆ 𝗚𝗲(bs)
h : (b = b ∨ b ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(b) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
no goals