proposition: Lemma agP w : reflect (cAG e p w) (AGb w).
proof: Proof. rewrite /AGb; apply (iffP idP). - move: w. cofix agP => w. rewrite (gfpE AR_mono) !inE. case/andP => [x1 x2]. apply: AGs _ => [//|v wv]. apply: agP. exact: (forall_inP x2). - apply: gfp_ind2 => {w} - w X CH. case => pw H. rewrite inE pw /=. apply/forall_inP => v /H. exact: CH. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)