proposition: Lemma doubleI_tdef2_unique T f g : doubleI_fix2 T f -> doubleI_fix2 T g -> f =2o g.
proof: Proof. move => fp gp. have H a b h: ordinalp a -> ordinalp b -> (doubleI_restr2 h a b) = restriction1 (doubleI_restr h a b) (doubleI_F a b). move => oa ob. have ss: sub (doubleI_F a b) (doubleI_E a b). by move => t tF; apply/setU2_P; left. have [ff _]: surjection (doubleI_restr h a b) by apply: Lfs_surjective. rewrite (Lfs_restriction1 ff); last by rewrite Lfs_source. by apply: Lfs_exten => t tE; rewrite (Lfs_V _ (ss _ tE)). pose T' a b h := T a b (restriction1 h (doubleI_F a b)) . apply:(doubleI_tdef_unique (T := T')) => a b oa ob. by rewrite (fp _ _ oa ob) (H _ _ _ oa ob) /T'. by rewrite (gp _ _ oa ob) (H _ _ _ oa ob). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)