proposition: Lemma many_der_unique C1 C2 f1 f2 (E1:= cnext C1) (E2:= cnext C2) (g1:= many_der f1 E1) (g2:= many_der f2 E2): C1 <=c C2 -> infinite_c C1 -> infinite_c C2 -> agrees_on E1 f1 f2 -> normal_function f1 E1 E1 -> normal_function f2 E2 E2 -> forall i, inc i E1 -> agrees_on E1 (Vf g1 i) (Vf g2 i).
proof: Proof. move => lcc ic1 ic2 agg n1 n2. have pa: sub E1 E2. move => x /(cnextP (proj1 ic1)) [sa sb]; apply/(cnextP (proj1 ic2)). split => //;exact: (cleT sb lcc). move: (many_der_ex ic1 n1). move: (many_der_ex ic2 n2). rewrite -/E1 -/E2 -/g1 -/g2. set ii1:= fun i => (intersectionf i (fun z => fixpoints (Vf g1 z))). set ii2:= fun i => (intersectionf i (fun z => fixpoints (Vf g2 z))). move => [fg2 sg2 g20 g2v [hr2 cc2 ng2 ig2]]. move => [fg1 sg1 g10 g1v [hr1 cc1 ng1 ig1]]. move => i ie1. have sg1i:source (Vf g1 i) = E1 by move: (ng1 _ ie1) => [[]]. have sg2i:source (Vf g2 i) = E2 by move: (ng2 _ (pa _ ie1)) => [[]]. hnf; rewrite sg1i sg2i; split=> // x xe1; move: x xe1. have oe1: ordinalp E1 by move:(cnext_pr1 (proj1 ic1)) => [[]]. have oi:= (Os_ordinal oe1 ie1). clear sg1i sg2i. move: i oi ie1; apply:least_ordinal2 => y oor etc ye1 x xe1. case: (equal_or_not y \0o) => ynz. by rewrite ynz g10 g20; move: agg => [sa sb sc];rewrite sc. rewrite g1v // g2v //; last by apply: pa. move: (cc1 y ye1 ynz) => [sa sc]. move: (cc2 y (pa _ ye1) ynz) => [sb sd]. have se: (ii1 y) = (ii2 y) \cap E1. have y0:= (olt_i (ord_ne0_pos oor ynz)). have yne: nonempty y by exists \0o. have lye1: y <o E1 by apply /oltP. set_extens t. move => ti. have te1: inc t E1. by move:(setIf_hi ti y0) => /Zo_S; rewrite g10; move: n1 => [[_ -> _ ]]. apply /setI2_P; split => //. apply /setIf_P => // j jy. have jy1: j <o y by apply /oltP. have je1:= olt_i (olt_ltT jy1 lye1). have sj1: (source (Vf g1 j)) = E1 by move: (ng1 _ je1) => [[]]. have sj2: (source (Vf g2 j)) = E2 by move: (ng2 _ (pa _ je1)) => [[]]. move:(setIf_hi ti jy) => /Zo_P [za zb]; apply /Zo_P; split => //. by rewrite sj2; apply: pa. by move: (etc _ jy1 je1 t te1) => <-. move => /setI2_P [ti2 te1]; apply /setIf_P => // j jy. have jy1: j <o y by apply /oltP. have je1:= olt_i (olt_ltT jy1 lye1). have sj1: (source (Vf g1 j)) = E1 by move: (ng1 _ je1) => [[]]. have sj2: (source (Vf g2 j)) = E2 by move: (ng2 _ (pa _ je1)) => [[]]. move:(setIf_hi ti2 jy) => /Zo_P [za zb]; apply /Zo_P; split => //. by rewrite sj1. by move: (etc _ jy1 je1 t te1) ->. move: (ordinals2_extc ic1 ic2 sa sb sc sd lcc se) => [ra rb rc]. by apply: rc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)