proposition: Lemma CNF_psi_unique p1 n p2 m: natp n ->natp m -> CNF_psi_ax p1 n -> CNF_psi_ax p2 m -> CNF_psiv p1 n = CNF_psiv p2 m -> n = m /\ same_below p1 p2 n.
proof: Proof. move => nN mN sa sb sc. move: (CNFr_unique (CNF_psi_p1 sa) (CNF_psi_p1 sb) nN mN sc) => [sd se]. split; [ exact | move => i lin]. move: (lin); rewrite sd => lim. move: (proj1 sa _ lin) (proj1 sb _ lim) => [{3}<- o1 o2] [{3}<- o3 o4]. move:(f_equal oopow (se _ lin)). rewrite /CNF_from_psi. rewrite {1}(odegree_psi o1 o2) (odegree_psi o3 o4). by move/ (Spsi_p4 o1 o3 o2 o4) =>[-> ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)