proposition: Lemma CNF_psi_exists_Gamma0 x: x <o Gamma_0 -> exists p n, [/\ natp n, CNF_psi_ax2 p n & x = CNF_psiv p n].
proof: Proof. move => h; move: (CNF_psi_exists (proj31_1 h)) => [p [n [nN pb xv]]]. exists p,n => //; split => //; split; first by exact. move => i idf. move: (CNFr_p3 nN (CNF_psi_p1 pb) idf). rewrite /CNF_from_psi. move:(proj1 pb _ idf) => [ _ pd pe]. rewrite (odegree_psi pd pe). rewrite -/(CNF_psiv p n) - xv => l1; move: (ole_ltT l1 h) => ha. split. exact: (ole_ltT (Spsi_p2' pd pe) ha). exact: (ole_ltT (proj1 (Spsi_p2 pd pe)) ha). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)