proposition: Lemma doubleI_unique A B T f1 f2: ordinalp A -> ordinalp B -> doubleI_def A B T f1 -> doubleI_def A B T f2 -> f1 = f2.
proof: Proof. move => oA oB [f1a f1b f1c] [f2a f2b f2c]. apply: function_exten4 => //; first ue. set U := Zo A (fun a => forall b, inc b B -> Vf f1 (J a b) = Vf f2 (J a b)). suff UA: U = A. hnf; rewrite f1b => p /setX_P [pp pa pb]; rewrite - pp. by move: pa; rewrite - UA => /Zo_P [pa pc]; apply: pc. apply: extensionality; first by apply: Zo_S. move => t tA; ex_middle tU. move: (least_ordinal3 (Os_ordinal oA tA) tU (p := fun z => inc z U)). set y := least_ordinal _ _; move=> [oy ynU ym]. case: (oleT_el oA oy) => cAy. by apply: ym; apply:olt_leT cAy; apply/(oltP oA). have yA: inc y A by apply/(oltP oA). case: ynU; apply/Zo_P; split; first exact. set V := Zo B (fun b => Vf f1 (J y b) = Vf f2 (J y b)). move => b bB; case: (inc_or_not b V); first by case /Zo_P. move => nbV. move: (least_ordinal3 (Os_ordinal oB bB) nbV (p := fun z => inc z V)). set z := least_ordinal _ _; move=> [oz znV zm]. case: (oleT_el oB oz) => cBz. by case: nbV; apply: zm; apply:olt_leT cBz; apply/(oltP oB). have zB: inc z B by apply/(oltP oB). have pab:inc (J y z) (A \times B) by apply: setXp_i. case: znV; apply/Zo_P; split => //. rewrite (f1c _ pab) (f2c _ pab); congr T; aw. set E := doubleI_E y z. have sx1: sub E (source f1) by rewrite f1b; apply:doubleI_E_sub. have sx2: sub E (source f2) by rewrite f2b - f1b. move: (restriction1_fs (proj1 f1a) sx1) (restriction1_fs (proj1 f2a) sx2). move => sj1 sj2. apply: function_exten4 => //; first by rewrite/restriction1; aw. rewrite {1}/restriction1; aw; move => x xE /=. rewrite (restriction1_V (proj1 f1a) sx1 xE) (restriction1_V (proj1 f2a) sx2 xE). case/setU2_P: xE. case/setU2_P. move => /setX_P [pp /set1_P px qx]; rewrite - pp px. have: inc (Q x) V by apply: zm; apply/(oltP oz). by move/Zo_P =>[_]. move => /setX_P [pp px /set1_P qx]. have: inc (P x) U by apply: ym; apply/(oltP oy). move/Zo_P => [pa pb]; rewrite - pp; apply: pb; apply/(oltP oB). by rewrite qx. move => /setX_P[px xy xz]. have: inc (P x) U by apply: ym; apply/(oltP oy). move/Zo_P => [pa pb]; rewrite - px; apply: pb; apply/(oltP oB). by apply: olt_ltT cBz; apply/(oltP oz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)