simp_all
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : [] ⊆ tail✝ → 𝗚𝗲([]) ⊆ 𝗚𝗲(tail✝)
h : [] ⊆ head✝ :: tail✝
⊢ 𝗚𝗲([]) ⊆ 𝗚𝗲(head✝ :: tail✝)
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
⊢ 𝗞 ⊆ 𝗴𝗲(head✝) ∪ 𝗚𝗲(tail✝)