cases h
case mk.mk
m n i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
j : Nat
hj' : j < m
hj : ↑{ val := j, isLt := hj' } < n
h : restrict { val := i, isLt := hi' } hi = restrict { val := j, isLt := hj' } hj
⊢ { val := i, isLt := hi' } = { val := j, isLt := hj' }
case mk.mk.refl
m n i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
hj' : i < m
hj : ↑{ val := i, isLt := hj' } < n
⊢ { val := i, isLt := hi' } = { val := i, isLt := hj' }