proposition: Lemma FixFun_fix_partial_iter : forall A (R:binary A) (P:A->Prop) B {IB:Inhab B} (F:(A->B)->(A->B)) (f:A->B), f = FixFun F -> wf R -> rec_contractive_noinv eq P F R -> (forall n x, P x -> f x = func_iter n F f x).
proof: Proof. Proof using. introv Def Wf Cont. lets~ M: FixFun_fix_partial Cont. rewrite <- Def in M. intros n. induction n. { auto. } { intros x Px. simpl. applys eq_trans (F f x). { applys~ M. } { applys~ Cont. } } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)