proposition: Lemma lfp_ind_aux (P : {fset T} -> Type) : P fset0 -> (forall s , P s -> P (F s)) -> P lfp.
proof: Proof. move => P0 Pn. rewrite /lfp. elim: (size U) => //= n. exact: Pn. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)