aesop
V : Type ?u.8297
inst✝ : SetTheory V
n : Nat
α : Sort u_1
l : Fin n → α
x : α
⊢ (if h : n < n then l { val := n, isLt := (_ : { val := n, isLt := (_ : n < Nat.succ n) }.val < n) } else x) = x
no goals