proposition: Lemma auP w : reflect (cAU e p q w) (AUb w).
proof: Proof. rewrite /AUb; apply: (iffP idP). - move: w. pattern (lfp AU_fun). apply: lfp_ind; first by move => ?; rewrite inE. move => X IH w. case/setUP; rewrite !inE; first by move => ?; exact: AU0. case/andP => ? A. apply: AUs => // v wv. apply: IH. exact: (forall_inP A). - rewrite (lfpE AU_mono). elim => {w} - w; first by rewrite !inE => ->. move => pw _ /forall_inP IH. by rewrite !inE (lfpE AU_mono) pw IH /=. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)