proposition: Lemma lfp_level_aux x : x \in lfp -> exists n, x \in iter n.+1 F fset0.
proof: Proof. Proof using F_mono. move => lf. exists (size U). apply/subP : lf. exact: iterFsub1. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)