proposition: Lemma gfp_ind (P : T -> Type) : (forall x X, (forall y, y \in U -> P y -> y \in X) -> P x -> x \in F X) -> forall x, x \in U -> P x -> x \in gfp.
proof: Proof. Proof using F_bound. move => H. apply gfp_ind_aux => [//|*]. exact: H. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)