proposition: Lemma CNFbB_prop n e c (X := Lg n (fun i => J (e i) (c i))): CNFb_ax gamma e c n -> natp n -> CNFB_ax X /\ CNFBv X = CNFbv gamma e c n.
proof: Proof. move => ax nN. move:(ax) => [[a1 a2 a3 a4] a5]; rewrite /X. rewrite /CNFB_ax /CNFBv Lgd. set e1:= oexp _; set c1:= ocoef _ . have h1: same_below e e1 n. by move => i /(NltP nN) lin; rewrite /e1/oexp LgV//; aw. have h2: same_below c c1 n. by move => i /(NltP nN) lin; rewrite /c1/ocoef LgV//; aw. move: (CNFb_exten h1 h2 ax nN) => [sa <-]. split; [split; [fprops | done | | exact ] | exact]. by move => i iin; rewrite LgV//; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)