proposition: Lemma gfp_ind (P : {set T} -> Type) : P setT -> (forall s , P s -> P (F s)) -> P gfp.
proof: Proof. move => H1 H2. rewrite /gfp /F'. apply lfp_ind => [|A]; rewrite ?setC0 ?setCK //. exact: H2. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)