proposition: Lemma segerberg s : mprv (AG (s ---> AX s) ---> s ---> AG s).
proof: Proof. apply: rAIL. apply: rAG_ind; last exact: axAEr. rewrite -> axAGE at 1. do 2 rule axAcase. do 3 Intro. rewrite <- axABBA. ApplyH axAI. by Apply* 2. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions