proposition: Lemma the_CNF_p3 e c n: CNFb_ax gamma e c n -> natp n -> the_CNFB (CNFbv gamma e c n) = Lg n (fun i => J (e i) (c i)).
proof: Proof. move => ax nN. have ox:=(OS_CNFq nN (proj1 ax)). move:(CNFbB_prop ax nN) (the_CNF_p0 ox) => [sa sb] [sc sd]. rewrite - sd in sb. symmetry; exact: (CNFB_unique sa sc sb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)