rw [proofIrrel xascend _]
case refl
α : Type u
r : α → α → Prop
β : α → Type v
x y : KVChain r β
xs : List (Sigma β)
xascend ascend✝ : List.Ascending (Sigma.relOnFst r) xs
⊢ { toList := xs, ascend := xascend } = { toList := xs, ascend := ascend✝ }
no goals