proposition: Lemma the_CNF_simplP x (z := the_CNF_simpl x): \0o <o x -> CNF_simple_ax (P z) (P (Q z)) (Q (Q z)) x.
proof: Proof. move => xp. set E := (osucc x \times (Nat \times x)). set p := (fun z => (CNF_simple_ax (P z) (P (Q z)) (Q (Q z)) x)). have ha: (exists2 z, inc z E & p z). move:(CNF_simple_exists xp) => [a [n [b h]]]. move: (CNF_simple_bnd h) => h'; exists (J a (J n b)) => //. by rewrite /p; aw. have hb:singl_val2 (inc^~ E) p. move => z' z'' /setX_P [qa qb /setX_P [qc qd qe]] az za' az'. move: za' => /setX_P [qa' qb' /setX_P [qc' qd' qe']]. move:(CNF_simple_unique az az') => [e1 e2 e3]. by rewrite - qa - qa' - qc - qc' e1 e2 e3. exact: (proj1 (@select_pr p E ha hb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)