proposition: Lemma gfp_ind2 (P : T -> Type) : (forall x (X : {set T}), (forall y, P y -> y \in X) -> P x -> x \in F X) -> forall x, P x -> x \in gfp.
proof: Proof. move => H. apply gfp_ind => [x|*]; first by rewrite inE. exact: H. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)