n n✝ : ℕ
α✝ β✝ : TypeVec n✝
⊢ (id ⊗' id) = id
n : ℕ
⊢ ∀ {n : ℕ} {α β : TypeVec n}, (id ⊗' id) = id
intros
case a.h
n n✝ : ℕ
α✝ β✝ : TypeVec n✝
i : Fin2 n✝
a : (α✝ ⊗ β✝) i
⊢ (id ⊗' id) i a = id i a
n n✝ : ℕ
α✝ β✝ : TypeVec n✝
⊢ (id ⊗' id) = id
ext (i a)
case a.h.fz
n n✝¹ : ℕ
α✝¹ β✝¹ : TypeVec n✝¹
i : Fin2 n✝¹
a✝ : (α✝¹ ⊗ β✝¹) i
n✝ : ℕ
α✝ β✝ : TypeVec (succ n✝)
a : (α✝ ⊗ β✝) Fin2.fz
⊢ (id ⊗' id) Fin2.fz a = id Fin2.fz a

case a.h.fs
n n✝¹ : ℕ
α✝¹ β✝¹ : TypeVec n✝¹
i : Fin2 n✝¹
a✝¹ : (α✝¹ ⊗ β✝¹) i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec n✝} (a : (α ⊗ β) a✝), (id ⊗' id) a✝ a = id a✝ a
α✝ β✝ : TypeVec (succ n✝)
a : (α✝ ⊗ β✝) (Fin2.fs a✝)
⊢ (id ⊗' id) (Fin2.fs a✝) a = id (Fin2.fs a✝) a
case a.h
n n✝ : ℕ
α✝ β✝ : TypeVec n✝
i : Fin2 n✝
a : (α✝ ⊗ β✝) i
⊢ (id ⊗' id) i a = id i a
induction' i with _ _ _ i_ih
case a.h.fz.mk
n n✝¹ : ℕ
α✝¹ β✝¹ : TypeVec n✝¹
i : Fin2 n✝¹
a : (α✝¹ ⊗ β✝¹) i
n✝ : ℕ
α✝ β✝ : TypeVec (succ n✝)
fst✝ : last α✝
snd✝ : last β✝
⊢ (id ⊗' id) Fin2.fz (fst✝, snd✝) = id Fin2.fz (fst✝, snd✝)
case a.h.fz
n n✝¹ : ℕ
α✝¹ β✝¹ : TypeVec n✝¹
i : Fin2 n✝¹
a✝ : (α✝¹ ⊗ β✝¹) i
n✝ : ℕ
α✝ β✝ : TypeVec (succ n✝)
a : (α✝ ⊗ β✝) Fin2.fz
⊢ (id ⊗' id) Fin2.fz a = id Fin2.fz a
cases a
no goals
case a.h.fz.mk
n n✝¹ : ℕ
α✝¹ β✝¹ : TypeVec n✝¹
i : Fin2 n✝¹
a : (α✝¹ ⊗ β✝¹) i
n✝ : ℕ
α✝ β✝ : TypeVec (succ n✝)
fst✝ : last α✝
snd✝ : last β✝
⊢ (id ⊗' id) Fin2.fz (fst✝, snd✝) = id Fin2.fz (fst✝, snd✝)
rfl
no goals
case a.h.fs
n n✝¹ : ℕ
α✝¹ β✝¹ : TypeVec n✝¹
i : Fin2 n✝¹
a✝¹ : (α✝¹ ⊗ β✝¹) i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α β : TypeVec n✝} (a : (α ⊗ β) a✝), (id ⊗' id) a✝ a = id a✝ a
α✝ β✝ : TypeVec (succ n✝)
a : (α✝ ⊗ β✝) (Fin2.fs a✝)
⊢ (id ⊗' id) (Fin2.fs a✝) a = id (Fin2.fs a✝) a
apply i_ih