proposition: Lemma CNFr_unique f g n m: CNFr_ax f n -> CNFr_ax g m -> natp n -> natp m -> CNFrv f n = CNFrv g m -> (n = m /\ same_below f g n).
proof: Proof. move => p1 p2 p3 p4; move: n p3 m p1 p2 p4; apply: Nat_induction. move => m af ag mN sv; split; last by move => i /clt0 h; case h. symmetry;ex_middle bad. by move: (CNFr_p6 mN ag bad); rewrite - sv CNFr_p5; case. move => n nN Hrec m af ag mN sv. case: (equal_or_not m \0c) => mz. by move: (CNFr_p6 (NS_succ nN) af (@succ_nz n)); rewrite sv mz CNFr_p5; case. move: (cpred_pr mN mz); set m':= (cpred m); move => [m'N mv]. rewrite mv in ag sv. move: (CNFr_ax_s nN af) (CNFr_ax_s m'N ag) => ax1 ax2. move: sv (CNFr_p4' nN af (m:= g m')) (CNFr_p4' m'N ag (m:= f n)). move:(CNFr_p2 nN af) (CNFr_p2 m'N ag). rewrite (CNFr_rec _ nN) (CNFr_rec _ m'N). move => le1 le2 eq1 lt1 lt2. move: (cltS nN) (cltS m'N) => ns1 ns2. case (oleT_ell (proj1 af _ ns1) (proj1 ag _ ns2)). + move => eq2. rewrite eq2 in eq1. move: (osum2_simpl (OS_CNFr0 nN ax1) (OS_CNFr0 m'N ax2) (proj31 le2) eq1). move / (Hrec m' ax1 ax2 m'N)=> [ra rb]. rewrite mv -ra; split; [ reflexivity | move => i /(cltSleP nN) li]. case (equal_or_not i n); first by move => ->; rewrite eq2 ra. by move => ni; apply:rb; split. + move /lt1; rewrite eq1 => /(oleNgt le2); case. + by move /lt2; rewrite - eq1 => /(oleNgt le1); case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)