proposition: Lemma inl_subsets_prop_I2v S S' M (H:inl_subfam_hyp S M) (H':inl_subfam_hyp S' M) : inl_same_data S S' -> inl_same_data (inductive_system_subsets H) (inductive_system_subsets H').
proof: Proof. move:(inl_subsets_prop H) => [ra rb rc rd]. move:(inl_subsets_prop H') => [ra' rb' rc' rd']. rewrite /inl_same_data ra rc rd ra' rc' rd' => - [ea eb ec]. by rewrite /inl_subfam_fct eb ec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)