law sorted_append

bend-mathlib@0.8.1.0 · list.bend:1061

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

1061# Appending two Nat lists sorted by Nat.is_le, with every element of the first <= every element of the second, gives a sorted list.
1062law sorted_append:
1063  for xs: List<&2, Nat>
1064  for ys: List<&2, Nat>
1065  for bnd: @x: Nat -> @y: Nat -> mem(~Nat, ~Nat.is_eq, x, xs) -> mem(~Nat, ~Nat.is_eq, y, ys) -> MNat.le(x, y)
1066  for hx: sorted_by(~Nat, ~Nat.is_le, xs)
1067  for hy: sorted_by(~Nat, ~Nat.is_le, ys)
1068  sorted_by(~Nat, ~Nat.is_le, List.append(&2, Nat, xs, ys))