proposition: Theorem rec_fixed_point : forall A B {IB:Inhab B} (F:(A->B)->(A->B)) (R:binary A) (P:A->Prop) (S:A->B->Prop) (E:binary B), equiv E -> (forall x, pred_compatible E (S x)) -> wf R -> rec_contractive E P F R S -> exists (f:A->B), partial_fixed_point E F (Build_partial f P) /\ (forall x, P x -> S x (f x)).
proof: Proof. Proof using. introv IB Equiv Comp WfR Cont. sets M: (rec_family E P R). sets Q: (fun x f => P x -> S x (f x)). forwards (f&Fixf&Qf): (>> cofe_fixed_point A (A->B) M F Q). typeclass. apply~ rec_cofe. introv Limu Qiui Ki Pi. applys Comp. apply~ Qiui. apply~ equiv_sym. apply~ Limu. apply~ rec_contractive_as_contractive. asserts Equ: (pfun_equiv E P = similar M). apply fun_ext_2. intros f1 f2. unfold M, similar, pfun_equiv. apply prop_ext. simpl. split~. exists (Build_partial f P). destruct Fixf as [Fixf _]. split~. unfold partial_fixed_point. simpl. rewrite~ Equ. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)