proposition: Lemma AG_strengthen (p1 p2 : X -> Prop) w : (forall v, p1 v -> p2 v) -> cAG p1 w -> cAG p2 w.
proof: Proof. move => H1. move: w. cofix AG_strengthen => w. case => [/H1 p2w IH]. by apply: AGs p2w _ => v /IH /AG_strengthen. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)