proposition: Lemma cnf_singleton1 e: ordinalp e -> cnf_and_val (Lg \1c (fun _: Set => (J e \1o))) (oopow e).
proof: Proof. move => oe; move: (cnf_one_term oe PN1). by rewrite (oprod1r (OS_oopow oe)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)