simp [appendr]
case h
α✝ : Type ?u.62895
m✝ : Type u → Type v
inst✝ : Monad m✝
α : Type w
β : Type u
m n : ℕ
x : α
v : Fin n → α
w : Fin m → α
i : Fin (m + n.succ)
⊢ appendr (x :> v) w i = (x :> appendr v w) i
no goals