case cons.cons a as iha b bs ihb =>
  simp_all;
  constructor;
  . cases h.1;
    . subst_vars; tauto;
    . apply Set.subset_union_of_subset_right $ mem (by assumption);
  . simpa using (iha h.2);
α : 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 :: as ⊆ bs → 𝗚𝗲(a :: as) ⊆ 𝗚𝗲(bs)
h : a :: as ⊆ b :: bs
⊢ 𝗚𝗲(a :: as) ⊆ 𝗚𝗲(b :: bs)
no goals