proposition: Lemma prl_subsets_prop_Iv S M (H:prl_subfam_hyp S M) (H':prl_subfam_hyp S M) : prl_same_data (projective_system_subsets H) (projective_system_subsets H').
proof: Proof. move:(prl_subsets_prop H) => [ra rb rc rd]. move:(prl_subsets_prop H') => [ra' rb' rc' rd']. by rewrite /prl_same_data ra rc rd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)