case fz
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ y✝ : α✝ i
n✝ : ℕ
α : TypeVec (succ n✝)
x y : α Fin2.fz
⊢ ofRepeat (repeatEq α Fin2.fz (prod.mk Fin2.fz x y)) ↔ x = y

case fs
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ y✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} {x y : α a✝}, ofRepeat (repeatEq α a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec (succ n✝)
x y : α (Fin2.fs a✝)
⊢ ofRepeat (repeatEq α (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x y)) ↔ x = y
n : ℕ
α : TypeVec n
i : Fin2 n
x y : α i
⊢ ofRepeat (repeatEq α i (prod.mk i x y)) ↔ x = y
induction' i with _ _ _ i_ih
case fs
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ y✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} {x y : α a✝}, ofRepeat (repeatEq α a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec (succ n✝)
x y : α (Fin2.fs a✝)
⊢ ofRepeat (repeatEq α (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x y)) ↔ x = y
case fz
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ y✝ : α✝ i
n✝ : ℕ
α : TypeVec (succ n✝)
x y : α Fin2.fz
⊢ ofRepeat (repeatEq α Fin2.fz (prod.mk Fin2.fz x y)) ↔ x = y

case fs
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ y✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} {x y : α a✝}, ofRepeat (repeatEq α a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec (succ n✝)
x y : α (Fin2.fs a✝)
⊢ ofRepeat (repeatEq α (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x y)) ↔ x = y
rfl
no goals
case fs
n : ℕ
α✝ : TypeVec n
i : Fin2 n
x✝ y✝ : α✝ i
n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec n✝} {x y : α a✝}, ofRepeat (repeatEq α a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec (succ n✝)
x y : α (Fin2.fs a✝)
⊢ ofRepeat (repeatEq α (Fin2.fs a✝) (prod.mk (Fin2.fs a✝) x y)) ↔ x = y
erw [repeatEq, i_ih]