α : Type u
m n o : ℕ
m' : Type ?u.49849
n' : Type ?u.49852
o' : Type ?u.49855
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (bit1 i) = (vecCons x u ∘ bit1) i
α : Type u
m n o : ℕ
m' : Type ?u.49849
n' : Type ?u.49852
o' : Type ?u.49855
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (bit1 i) =
    vecAlt1 (_ : Nat.succ n + Nat.succ n = Nat.succ n + Nat.succ n)
      (vecAppend (_ : Nat.succ n + Nat.succ n = Nat.succ n + Nat.succ n) (vecCons x u) (vecCons x u)) i
rw [vecAlt1_vecAppend]
no goals
α : Type u
m n o : ℕ
m' : Type ?u.49849
n' : Type ?u.49852
o' : Type ?u.49855
x : α
u : Fin n → α
i : Fin (n + 1)
⊢ vecCons x u (bit1 i) = (vecCons x u ∘ bit1) i
rfl