proposition: Lemma inl_dl_S_lambda_Iv2 x y (H1: inc x I2) (H2: inc y I2) : x = y -> inl_same_data (inl_dl_S_lambda H1)(inl_dl_S_lambda H2).
proof: Proof. move => exy. move:(inl_dl_S_lambda_prop H1) (inl_dl_S_lambda_prop H2). rewrite /inl_same_data. by move => [ -> _ -> ->] [ -> _ -> ->]; rewrite exy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)