proposition: Lemma value_inj f g: inc f dexpansions -> inc g dexpansions-> value f = value g -> f = g.
proof: Proof. move: f g. suff: forall n, natp n -> forall f g, size f <=c n -> size g <=c n -> inc f dexpansions -> inc g dexpansions -> value f = value g -> f = g. move => H f g ft gt. move:(size_p ft) (size_p gt) => /proj31 sN /proj31 sN' sv. move: (Nmax_p1 sN sN') =>[qa qb qc]. exact:(H _ qa f g qb qc ft gt sv). apply: Nat_induction. move => f g /cle0 s1z /cle0 s2z ft gt sv. move:(size_p ft)(size_p gt) =>[qa qb qc][qd qe qf]. move: ft gt => /Zo_S /functionsP [ff sf tf]/Zo_S /functionsP [fg sg tg]. apply: (function_exten ff fg); (try ue); rewrite sf => t tN. have sa: size f <=c t by rewrite s1z; apply: cle0n. have sb: size g <=c t by rewrite s2z; apply: cle0n. by rewrite (qb _ tN sa) (qe _ tN sb). move => n nN Hrec f g ls1 ls2 ft gt sv. move: (shift_p1 ft)(shift_p1 gt) => [f1t sf1] [f2t sg2]. move:(proj31 (size_p ft)) (proj31 (size_p gt)) => sfN sgN. have h1: size (shift f) <=c n. rewrite sf1; case: (equal_or_not (size f) \0c) => qa. by rewrite qa cpred0 ; apply:cle0n. move: (cpred_pr sfN qa) => [qc qd]. apply/(cleSSP (CS_nat qc) (CS_nat nN)); ue. have h2: size (shift g) <=c n. rewrite sg2; case: (equal_or_not (size g) \0c) => qa. by rewrite qa cpred0 ; apply:cle0n. move: (cpred_pr sgN qa) => [qc qd]. apply/(cleSSP (CS_nat qc) (CS_nat nN)); ue. move: (shift_val ft) (shift_val gt). rewrite csumC (csumC (Vf g \0c)). move:(value_nat f1t) (value_nat f2t). set v1 := value _ ; set v2 := value _ => vfN vgN eq1 eq2. move:(value_nat ft) => vN. move/Zo_S:ft => /functionsP[ff sf tf]. move/Zo_S:gt => /functionsP[fg sg tg]. have aux t: inc t C2 -> t <c \2c. case/set2_P => -> -; [ apply: clt_02 | apply: clt_12]. have fsm: Vf f \0c <c \2c. have /aux //: inc (Vf f \0c) C2 by Wtac; rewrite sf; apply: NS0. have gsm: Vf g \0c <c \2c. have /aux //: inc (Vf g \0c) C2 by Wtac; rewrite sg; apply: NS0. move:(NS_lt_nat fsm NS2) (NS_lt_nat gsm NS2) => fsN gsN. have d1p: cdivision_prop (value f) \2c v1 (Vf f \0c) by split. have d2p: cdivision_prop (value g) \2c v2 (Vf g \0c) by split. rewrite - sv in d2p. move: (cdivision_unique vN NS2 vfN fsN vgN gsN card2_nz d1p d2p) =>[ra rb]. move:(Hrec _ _ h1 h2 f1t f2t ra) => rc. apply: (function_exten ff fg); (try ue); rewrite sf => x xN. case: (equal_or_not x \0c) => xz; first by rewrite xz; apply: rb. move: (cpred_pr xN xz) =>[pN pv]. move:(f_equal (Vf ^~ (cpred x)) rc); rewrite /shift ! LfV; trivial. - by rewrite - pv. - by move => t /NS_succ tN; Wtac; ue. - by move => t /NS_succ tN; Wtac; ue. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)