proposition: Lemma rAGp_ind (k : ksSystem) (u s : k) : mprv (u ---> AX (u :/\: s)) -> mprv (u ---> AX (AG s)).
proof: Proof. move => H /=. rewrite -> H. apply: rNorm. apply: rAG_ind; last exact: axAEr. rewrite <- H. exact: axAEl. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions