proposition: Fact cAG_crt p w : cAG p w <-> forall v, clos_refl_trans e w v -> p v.
proof: Proof. split. - move => C v H. apply clos_rt_rt1n in H. by elim: H C => [x|x y z xy _ IH]; case => // _ /(_ _ xy). - move: w. cofix cAG_crt => w H. apply: AGs; first by apply H,rt_refl. move => v wv. apply: cAG_crt => v' vv'. apply: H. eauto using rt_step, rt_trans. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)