def pf_left

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/array.bend:97

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

97def pf_left(-T: Data, +p: Nat, +l: Tree<T>, +r: Tree<T>, +pf: {perfect(T, 1n+p, TNode{l, r}) == True{} : Bool}) -> {perfect(T, p, l) == True{} : Bool}:
98  L.and_left(perfect(T, p, l), perfect(T, p, r), pf)