def internal_sorted_tail_step

bend-mathlib@0.8.1.0 · sort.bend:21

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat
import bend-mathlib@0.8.1.0/list.bend as MList

21def internal_sorted_tail_step(~A: Data, ~le: A -> A -> Bool, -x: A, +y: A, +t: List<&2, A>, b: Bool, e: {le(x, y) == b : Bool}, h: MList.sorted_by(~A, ~le, x <> y <> t)) -> MList.sorted_by(~A, ~le, y <> t):
22  match b:
23    case True{}:
24      Equal.trans(Bool, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), List.zip(&2, A, &2, A, y <> t, t)), List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), (x, y) <> List.zip(&2, A, &2, A, y <> t, t)), True{}, MList.internal_sorted_cons_true(~A, ~le, x, y, List.zip(&2, A, &2, A, y <> t, t), e), h)
25    case False{}:
26      Empty.absurd(MList.sorted_by(~A, ~le, y <> t), MNat.internal_false_ne_true(Equal.trans(Bool, False{}, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), (x, y) <> List.zip(&2, A, &2, A, y <> t, t)), True{}, MList.internal_sorted_cons_false(~A, ~le, x, y, List.zip(&2, A, &2, A, y <> t, t), e), h)))