proposition: Lemma doubleI_unique2 T A1 A2 B1 B2 f: A1 <=o A2 -> B1 <=o B2 -> doubleI_def A2 B2 T f -> doubleI_def A1 B1 T (restriction1 f (A1 \times B1)).
proof: Proof. move => le1 le2 [ha hb hc]. have sp1: sub (A1 \times B1) (A2 \times B2). apply: setX_Slr; [ exact (proj33 le1) | exact (proj33 le2)]. have sp2:sub (A1 \times B1) (source f) by ue. have rs1 :=(restriction1_fs (proj1 ha) sp2). split. exact. by rewrite /restriction1; aw. move => p pAB. rewrite (restriction1_V (proj1 ha) sp2 pAB). rewrite (hc _ (sp1 _ pAB));congr T. have sp3: sub (doubleI_E (P p) (Q p)) (A1 \times B1). move/setX_P: pAB => [_ pa qbØ]. by apply: (doubleI_E_sub (proj31 le1) (proj31 le2)). have sp4:= sub_trans sp3 sp2. rewrite (Lfs_restriction1 (proj1 ha) (sub_trans sp3 sp2)). rewrite (Lfs_restriction1 (proj1 rs1)); last by rewrite /restriction1; aw. by apply:Lfs_exten => t ts; rewrite (restriction1_V (proj1 ha) sp2 (sp3 _ ts)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)