simp_all
case cons
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h : x ∈ a :: as
⊢ 𝗴𝗲(x) ⊆ 𝗚𝗲(a :: as)
case cons
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h : x = a ∨ x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)