proposition: Lemma CNF_singleton c0 e0 (c:= fun _: Set => c0)(e:= fun _: Set => e0): ordinalp e0 -> c0 <o gamma -> \2c <=o gamma -> [/\ CNFq_ax e c \1c, CNFbv e c \1c = gamma ^o e0 *o c0 & (\0o <o c0 -> CNFb_ax e c \1c)].
proof: Proof. move=> oe co b2. have aux: CNFq_ax e c \1c. rewrite /e/c;split => // i ib. by rewrite - succ_zero;move/(cltSleP NS0)=> /(cltNge (@succ_positive i)). by rewrite (CNFq_p3 aux clt_01). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)