proposition: Lemma projective_limit_Iv S S': prl_same_data S S' -> projective_limit S = projective_limit S'.
proof: Proof. by move => [sa sb sc]; rewrite /projective_limit sa sb sc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)