induction l₁ generalizing l₂ <;> induction l₂
α : Type u_1
Ax : AxiomSet α
l₁ l₂ : List Axioms.Geach.Taple
h : l₁ ⊆ l₂
⊢ 𝗚𝗲(l₁) ⊆ 𝗚𝗲(l₂)
case nil.nil
α : Type u_1
Ax : AxiomSet α
h : [] ⊆ []
⊢ 𝗚𝗲([]) ⊆ 𝗚𝗲([])

case nil.cons
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : [] ⊆ tail✝ → 𝗚𝗲([]) ⊆ 𝗚𝗲(tail✝)
h : [] ⊆ head✝ :: tail✝
⊢ 𝗚𝗲([]) ⊆ 𝗚𝗲(head✝ :: tail✝)

case cons.nil
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : ∀ {l₂ : List Axioms.Geach.Taple}, tail✝ ⊆ l₂ → 𝗚𝗲(tail✝) ⊆ 𝗚𝗲(l₂)
h : head✝ :: tail✝ ⊆ []
⊢ 𝗚𝗲(head✝ :: tail✝) ⊆ 𝗚𝗲([])

case cons.cons
α : Type u_1
Ax : AxiomSet α
head✝¹ : Axioms.Geach.Taple
tail✝¹ : List Axioms.Geach.Taple
tail_ih✝¹ : ∀ {l₂ : List Axioms.Geach.Taple}, tail✝¹ ⊆ l₂ → 𝗚𝗲(tail✝¹) ⊆ 𝗚𝗲(l₂)
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : head✝¹ :: tail✝¹ ⊆ tail✝ → 𝗚𝗲(head✝¹ :: tail✝¹) ⊆ 𝗚𝗲(tail✝)
h : head✝¹ :: tail✝¹ ⊆ head✝ :: tail✝
⊢ 𝗚𝗲(head✝¹ :: tail✝¹) ⊆ 𝗚𝗲(head✝ :: tail✝)