proposition: Lemma mp2 s t u : mprv (s ---> t ---> u) -> mprv s -> mprv t -> mprv u.
proof: Proof. move => ax A B. by [mp; first mp; first apply ax]. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions