proposition: Lemma lfp_ind (P : {set T} -> Type) : P set0 -> (forall s , P s -> P (F s)) -> P lfp.
proof: Proof. move => P0 Pn. rewrite /lfp. set n := #|T|. elim: n => //= n. exact: Pn. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)