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