proposition: Lemma CNF_c_ax e c n c0 k: \0o <o c0 -> c0 <o gamma -> CNFb_ax e c n -> CNFb_ax e (cnf_c c k c0) n.
proof: Proof. move => c1 c2 [[p1 p2 p3 p4] p5]; rewrite/cnf_c. split; [split => // |]; move => i lin; Ytac cc => //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)