def internal_sorted_append_cons

bend-mathlib@0.8.1.0 · list.bend:1047

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

1047def internal_sorted_append_cons(t: List<&2, Nat>, ys: List<&2, Nat>, +x: Nat, bnd: @a: Nat -> @b: Nat -> mem(~Nat, ~Nat.is_eq, a, x <> t) -> mem(~Nat, ~Nat.is_eq, b, ys) -> MNat.le(a, b), hx: sorted_by(~Nat, ~Nat.is_le, x <> t), hy: sorted_by(~Nat, ~Nat.is_le, ys)) -> sorted_by(~Nat, ~Nat.is_le, x <> List.append(&2, Nat, t, ys)):
1048  match t:
1049    case Nil{}:
1050      match ys:
1051        case Nil{}:
1052          {==}
1053        case +y <> u:
1054          +u = u
1055          sorted_cons_cons_intro(x, y, u, bnd(x, y, mem_cons_self(x, Nil{}), mem_cons_self(y, u)), hy)
1056    case +z <> u:
1057      +u = u
1058      +hx = hx
1059      sorted_cons_cons_intro(x, z, List.append(&2, Nat, u, ys), sorted_cons_cons_elim_le(x, z, u, hx), internal_sorted_append_cons(u, ys, z, +a => b => ma => mb => bnd(a, b, mem_cons_of_mem(a, x, z <> u, ma), mb), sorted_cons_cons_elim_tail(x, z, u, hx), hy))