proposition: Lemma axAGN s t : mprv (AG (s ---> t) ---> AG s ---> AG t).
proof: Proof. apply: rAIL. apply: rAG_ind. - rewrite -> axAGEr at 1. by rewrite -> (axAGEr s),axABBA at 1. - rule axAcase. by do 2 rewrite -> axAGEl. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions