proposition: Lemma CNFb_unique (e1 c1:fterm) n1 (e2 c2:fterm) n2: natp n1 -> natp n2 -> CNFb_ax e1 c1 n1 -> CNFb_ax e2 c2 n2 -> CNFbv e1 c1 n1 = CNFbv e2 c2 n2 -> (n1 = n2 /\ forall i, i <c n1 -> e1 i = e2 i /\ c1 i = c2 i).
proof: Proof. move => n1N n2N; move: n1 n1N n2 n2N; apply: Nat_induction. move=> n2 n2N ax1 ax2. case: (equal_or_not n2 \0c) => n2z. by rewrite n2z => _; split => // i /clt0. move: (cpred_pr n2N n2z) => [mb mv] eq. rewrite mv in ax2 eq. by move: (proj2 (CNFq_pg5 mb ax2)); rewrite - eq CNFq_p2;case. move =>n1 n1N Hrec n2' n2'N ax1s ax2s sv. case: (equal_or_not n2' \0c) => n2z. by move: (proj2 (CNFq_pg5 n1N ax1s)); rewrite sv n2z CNFq_p2; case. move: (cpred_pr n2'N n2z) => []; set n2 := (cpred n2'); move => n2N n2v. rewrite n2v in ax2s sv. move: (cltS n1N) (cltS n2N) => lt1 lt2. move: (ax1s) (ax2s) => [[u1 u2 u3 u4] u5] [[v1 v2 v3 v4] v5]. move: (u2 n1 lt1) (v2 n2 lt2) (u3 n1 lt1) (v3 n2 lt2) => oa1 oa2 of1 of2. move: (u5 n1 lt1) (v5 n2 lt2) => ob1 ob2. move: (proj32_1 ob1) (proj32_1 ob2) => oc1 oc2. move: (CNFb_p5 n1N ax1s)(CNFb_p5 n2N ax2s) => ax1 ax2. move: (OS_CNFq n1N (proj1 ax1)) (OS_CNFq n2N (proj1 ax2)) => oe1 oe2. set a1 := CNFbv e1 c1 (csucc n1). set a2 := CNFbv e2 c2 (csucc n2). move: (erefl a1); rewrite {2} /a1 (CNFq_p1 _ _ n1N) => ha1. move: (erefl a2); rewrite {2} /a2 (CNFq_p1 _ _ n2N) => ha2. move: (CNFq_pg n1N (proj1 ax1s)) (CNFq_pg n2N (proj1 ax2s)) => hb1 hb2. have og1:=(OS_CNFq (NS_succ n1N) (proj1 ax1s)). have ox1: (ord_ext_div_pr gamma a1 (e1 n1) (c1 n1) (CNFbv e1 c1 n1)). split;[ exact | exact| exact | split; [exact: ha1 | exact | exact | exact]]. have ox2: (ord_ext_div_pr gamma a1 (e2 n2) (c2 n2) (CNFbv e2 c2 n2)). rewrite /a1 sv -/a2. split;[ exact | exact| exact | split; [exact: ha2 | exact | exact | exact]]. move: (ord_ext_div_unique u1 og1 ox1 ox2) => [se1 sc1 sr1]. move: (Hrec _ n2N ax1 ax2 sr1) => [n12 etc]; split. by rewrite n2v - n12. move => i /(cltSleP n1N); case: (equal_or_not i n1) => in1. by rewrite in1 {4 6} n12 => _; split. by move => nin1; move: (etc _ (conj nin1 in1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)