proposition: Lemma rIntro s t xs : mprv ((\and_(<- s :: xs) ---> t)) -> mprv (\and_(<- xs) ---> s ---> t).
proof: Proof. rewrite big_cons => H. rewrite <- H, <- axAC. exact: axAI. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions