proposition: Lemma kleene_lfp_fixed : f kleene_lfp = kleene_lfp.
proof: Proof. by rewrite (@contE _ _ f) lim_liftE; apply: limE; rewrite reindex. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)