proposition: Lemma axAcase (pS : pSystem) (u s t : pS) : mprv ((u ---> s ---> t) ---> (u :/\: s ---> t)).
proof: Proof. do 2 Intro. Apply* 1; by rewrite -> bigA1E. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions