. cases h.1;
  . subst_vars; tauto;
  . apply Set.subset_union_of_subset_right $ mem (by assumption);
case left
α : 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
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

case right
α : 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
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
case right
α : 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
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)