[GOAL]
n iv : ℕ
ilt₁ : iv < n
jv : ℕ
jlt₁ : jv < n
h : { val := iv, isLt := ilt₁ }.val = { val := jv, isLt := jlt₁ }.val
⊢ { val := iv, isLt := ilt₁ } = { val := jv, isLt := jlt₁ }
[PROOFSTEP]
cases h
[GOAL]
case refl
n iv : ℕ
ilt₁ jlt₁ : iv < n
⊢ { val := iv, isLt := ilt₁ } = { val := iv, isLt := jlt₁ }
[PROOFSTEP]
rfl
