proposition: Lemma arP w : reflect (cAR e p q w) (ARb w).
proof: Proof. rewrite /ARb; apply (iffP idP). - move: w. cofix arP => w. rewrite (gfpE AR_mono) !inE. case/orP => /andP [x1 x2]; first exact: AR0. apply: ARs => // v wv. apply: arP. exact: (forall_inP x2). - apply: gfp_ind2 => {w} - w X CH. case; first by rewrite !inE; bcase. move => qw H. rewrite inE; rightb; rewrite inE qw /=. apply/forall_inP => v /H. exact: CH. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)