cases h
α : Type u
r : α → α → Prop
β : α → Type v
x y : KVChain r β
xs : List (Sigma β)
xascend : List.Ascending (Sigma.relOnFst r) xs
ys : List (Sigma β)
ascend✝ : List.Ascending (Sigma.relOnFst r) ys
h : { toList := xs, ascend := xascend }.toList = { toList := ys, ascend := ascend✝ }.toList
⊢ { toList := xs, ascend := xascend } = { toList := ys, ascend := ascend✝ }
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✝ }