proposition: Lemma lfp_ind (P : T -> Type) : (forall x X, (forall y, y \in X -> P y) -> x \in F X -> P x) -> forall x, x \in lfp -> P x.
proof: Proof. move => H. apply lfp_ind_aux => [?| X IH x]; [by rewrite in_fset0| exact: H]. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)