case fz
n : ℕ
p : Prop
n✝ : ℕ
α : TypeVec (succ n✝)
x : α Fin2.fz
⊢ ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p

case fs
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ ofRepeat (TypeVec.const p α (Fin2.fs a✝) x) ↔ p
n : ℕ
α : TypeVec n
i : Fin2 n
x : α i
p : Prop
⊢ ofRepeat (TypeVec.const p α i x) ↔ p
induction i
case fs
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ ofRepeat (TypeVec.const p α (Fin2.fs a✝) x) ↔ p
case fz
n : ℕ
p : Prop
n✝ : ℕ
α : TypeVec (succ n✝)
x : α Fin2.fz
⊢ ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p

case fs
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ ofRepeat (TypeVec.const p α (Fin2.fs a✝) x) ↔ p
case fz       => rfl
no goals
case fs
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : ∀ {α : TypeVec n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ ofRepeat (TypeVec.const p α (Fin2.fs a✝) x) ↔ p
case fs _ ih  => erw [TypeVec.const, @ih (drop α) x]
no goals
n : ℕ
p : Prop
n✝ : ℕ
α : TypeVec (succ n✝)
x : α Fin2.fz
⊢ ofRepeat (TypeVec.const p α Fin2.fz x) ↔ p
rfl
no goals
n : ℕ
p : Prop
n✝ : ℕ
a✝ : Fin2 n✝
ih : ∀ {α : TypeVec n✝} {x : α a✝}, ofRepeat (TypeVec.const p α a✝ x) ↔ p
α : TypeVec (succ n✝)
x : α (Fin2.fs a✝)
⊢ ofRepeat (TypeVec.const p α (Fin2.fs a✝) x) ↔ p
erw [TypeVec.const, @ih (drop α) x]