induction l with
| nil => contradiction;
| cons a as ih =>
  simp_all;
  cases h;
  . subst_vars; tauto;
  . apply Set.subset_union_of_subset_right $ ih (by assumption);
α : Type u_1
Ax : AxiomSet α
x : Axioms.Geach.Taple
l : List Axioms.Geach.Taple
h : x ∈ l
⊢ 𝗴𝗲(x) ⊆ 𝗚𝗲(l)
no goals