proposition: Lemma doubleI_tdef_rec2 T: doubleI_fix2 T (doubleI_tdef2 T).
proof: Proof. move => a b oa ob. rewrite /doubleI_tdef2 (doubleI_tdef_rec _ oa ob);congr T. set f := doubleI_restr _ _ _. have sjf: surjection f by apply:Lfs_surjective. have sEF: sub (doubleI_F a b) (doubleI_E a b). by move => t tf; apply/setU2_P; left. have ss: sub (doubleI_F a b) (source f) by rewrite Lfs_source. rewrite (Lfs_restriction1 (proj1 sjf) ss). by apply: Lfs_exten => t tF; rewrite (Lfs_V _ (sEF _ tF)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)