proposition: Lemma axAReq s t : mprv (AR s t <--> t :/\: (s :\/: AX (AR s t))).
proof: Proof. rule axEI. - ApplyH axAI. exact: axARE. do 2 Intro. ApplyH axARu. - apply: rAR_ind; first exact: axAEl. rule axAcase; drop. rule axOE; first exact: axContra. rule axC; drop. apply: rNorm. ApplyH axAI. exact: axARE. exact: axARu. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions