proposition: Lemma prl_restr_Iv2 S S' J (h1: sub J (psI S))(h2: sub J (psI S')): prl_same_data S S' -> prl_same_data (prl_restr h1) (prl_restr h2).
proof: Proof. move => [ea eb ec]. move:(prl_restr_prop h1) => [pa pb pc pd]. move:(prl_restr_prop h2) => [pa' pb' pc' pd']. by rewrite /prl_same_data pa pc pd pa' pc' pd' ea eb ec. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)