proposition: Lemma doubleI_tdef_unique T f g : doubleI_fix1 T f -> doubleI_fix1 T g -> f =2o g.
proof: Proof. move => fp gp a b oa ob. set A := osucc a; set B := osucc b. set AB:= A \times B. have abAB: inc (J a b) AB. apply:setXp_i; rewrite /A/B; fprops. pose fv p := f (P p) (Q p); pose gv p := g (P p) (Q p); set F := Lfs fv AB; set G := Lfs gv AB. have ->: f a b = Vf F (J a b) by rewrite /F (Lfs_V _ abAB) /fv;aw. have ->: g a b = Vf G (J a b) by rewrite /G (Lfs_V _ abAB) /gv;aw. suff: F = G by move ->. have oA: ordinalp A by apply:OS_succ. have oB: ordinalp B by apply:OS_succ. have aux h: doubleI_fix1 T h -> doubleI_def A B (fun p => T (P p) (Q p)) (Lfs (fun p => h (P p) (Q p)) AB). move => hp. split; [ apply:Lfs_surjective | by rewrite Lfs_source | move => p pAB]. move/setX_P:(pAB) => [pp pxa pxb]. move:(Os_ordinal oA pxa) (Os_ordinal oB pxb) => op oq. rewrite (Lfs_V _ pAB) (hp _ _ op oq); congr T. move:(doubleI_E_sub oA oB pxa pxb) => ss. rewrite Lfs_restriction1 ?Lfs_source //. apply: Lfs_exten => t tE //;rewrite Lfs_V; fprops. apply:surj_function; apply:Lfs_surjective. exact: (doubleI_unique oA oB (aux _ fp) (aux _ gp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)