proposition: Lemma axABBA s t : mprv (AX s :/\: AX t <--> AX (s :/\: t)).
proof: Proof. rule axEI. - rule axAcase. rewrite <- axN. apply rNorm. exact: axAI. - Intro. ApplyH axAI; Rev; by apply rNorm. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions