proposition: Lemma rHyp1 s t : mprv (\and_(<- [:: s]) ---> t) -> mprv (s ---> t).
proof: Proof. move => H. by apply rHyp,rIntro. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions