proposition: Lemma doubleI_unique3 T A1 A2 B1 B2 f g: A1 <=o A2 -> B1 <=o B2 -> doubleI_def A2 B2 T f -> doubleI_def A1 B1 T g -> g = (restriction1 f (A1 \times B1)).
proof: Proof. move => ha hb hc hd. exact: (doubleI_unique (proj31 ha) (proj31 hb) hd (doubleI_unique2 ha hb hc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)