proposition: Lemma axAGE s : mprv (AG s <--> s :/\: AX (AG s)).
proof: Proof. have S: mprv (AG s ---> s :/\: AX (AG s)). rewrite -> (axA2 (AG s)) at 1. by rewrite -> axAGEl,axAGEr at 1. rule axEI => //. apply: rAG_ind; last exact: axAEl. rule axAcase. drop. exact: rNorm. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions