case refl
n : Nat
i : Fin n
⊢ (_ : n = n) ▸ i = { val := i.val, isLt := (_ : i.val < n) }
n n' : Nat
e : n = n'
i : Fin n
⊢ e ▸ i = { val := i.val, isLt := (_ : i.val < n') }
cases e
no goals
case refl
n : Nat
i : Fin n
⊢ (_ : n = n) ▸ i = { val := i.val, isLt := (_ : i.val < n) }
rfl