case a.h
n : ℕ
α β : TypeVec n
i : Fin2 n
x : (α ⊗ β) i
⊢ (id ⊗' id) i x = id i x
n : ℕ
α β : TypeVec n
⊢ (id ⊗' id) = id
ext i x : 2
case a.h.fz
n n✝ : ℕ
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) Fin2.fz
⊢ (id Fin2.fz x.fst, id Fin2.fz x.snd) = id Fin2.fz x

case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) (Fin2.fs a✝)
⊢ id a✝ x = id (Fin2.fs a✝) x
case a.h
n : ℕ
α β : TypeVec n
i : Fin2 n
x : (α ⊗ β) i
⊢ (id ⊗' id) i x = id i x
induction i <;> simp only [TypeVec.prod.map, *, dropFun_id]
case a.h.fz.mk
n n✝ : ℕ
α β : TypeVec (Nat.succ n✝)
fst✝ : last α
snd✝ : last β
⊢ (id Fin2.fz (fst✝, snd✝).fst, id Fin2.fz (fst✝, snd✝).snd) = id Fin2.fz (fst✝, snd✝)

case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) (Fin2.fs a✝)
⊢ id a✝ x = id (Fin2.fs a✝) x
case a.h.fz
n n✝ : ℕ
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) Fin2.fz
⊢ (id Fin2.fz x.fst, id Fin2.fz x.snd) = id Fin2.fz x

case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) (Fin2.fs a✝)
⊢ id a✝ x = id (Fin2.fs a✝) x
cases x
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) (Fin2.fs a✝)
⊢ id a✝ x = id (Fin2.fs a✝) x
case a.h.fz.mk
n n✝ : ℕ
α β : TypeVec (Nat.succ n✝)
fst✝ : last α
snd✝ : last β
⊢ (id Fin2.fz (fst✝, snd✝).fst, id Fin2.fz (fst✝, snd✝).snd) = id Fin2.fz (fst✝, snd✝)

case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) (Fin2.fs a✝)
⊢ id a✝ x = id (Fin2.fs a✝) x
rfl
no goals
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α β : TypeVec n✝} (x : (α ⊗ β) a✝), (id ⊗' id) a✝ x = id a✝ x
α β : TypeVec (Nat.succ n✝)
x : (α ⊗ β) (Fin2.fs a✝)
⊢ id a✝ x = id (Fin2.fs a✝) x
rfl