def pf_right

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

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

100def pf_right(-T: Data, +p: Nat, +l: Tree<T>, +r: Tree<T>, +pf: {perfect(T, 1n+p, TNode{l, r}) == True{} : Bool}) -> {perfect(T, p, r) == True{} : Bool}:
101  L.and_right(perfect(T, p, l), perfect(T, p, r), pf)