def all01_app

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bitsv.bend:37

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg

37def all01_app(xs: List<&2, Nat>, +ys: List<&2, Nat>, +hx: {all01(xs) == True{} : Bool}, +hy: {all01(ys) == True{} : Bool}) -> {all01(List.append(&2, Nat, xs, ys)) == True{} : Bool}:
38  match xs:
39    case Nil{}:
40      hy
41    case +x <> +t:
42      Lg.and_intro(Nat.is_lt(x, 2n), all01(List.append(&2, Nat, t, ys)), Lg.and_left(Nat.is_lt(x, 2n), all01(t), hx), all01_app(t, ys, Lg.and_right(Nat.is_lt(x, 2n), all01(t), hx), hy))