proposition: Lemma CNFp_unique p n p' n' : CNFp_ax p n -> CNFp_ax p' n' -> natp n -> natp n' -> CNFpv p n = CNFpv p' n' -> n = n' /\ same_below p p' (csucc n).
proof: Proof. move=> ax1 ax2 nN n'N eq. move: (CNFp_p4 ax1 nN) => [e1 [c1 [pa pb pc pe]]]. move: (CNFp_p4 ax2 n'N) => [e1' [c1' [pa' pb' pc' pe']]]. rewrite -pb -pb' in eq. move: (CNFb_unique (NS_succ nN) (NS_succ n'N) pa pa' eq) => [sa sb]. have nn:= (csucc_inj (CS_nat nN) (CS_nat n'N) sa). split; first exact. rewrite - nn in pc' pe'. move => i /(cltSleP nN); case/(cle_eqVlt)=> la. by rewrite la pe pe'; move:(sb _ (succ_positive n)) => [-> ->]. rewrite (pc _ la) (pc' _ la). move: (sb _ (clt_leT la (cleS nN))) => [-> _]. by move: (sb _ (cltSS la)) => [-> ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)