proposition: Lemma inl_same_dataT S S' S'' : inl_same_data S S' -> inl_same_data S' S'' -> inl_same_data S S''.
proof: Proof. by rewrite /inl_same_data; move => [-> -> ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)