proposition: Lemma gfp_ind_aux (P : {fset T} -> Type) : P U -> (forall s , P s -> P (F s)) -> P gfp.
proof: Proof. Proof using F_bound. move => PU Pn. rewrite /gfp /F'. apply lfp_ind_aux => [|A]; rewrite ?fsetD0 ?fsetCK ?F_bound //. exact: Pn. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)