proposition: Lemma rec_contractive_as_contractive : forall A B (E:binary B) (P:A->Prop) (F:(A->B)->(A->B)) (R:binary A) (S:A->B->Prop), equiv E -> (forall x, pred_compatible E (S x)) -> wf R -> rec_contractive E P F R S -> contractive (rec_family E P R) F (fun x f => P x -> S x (f x)).
proof: Proof. Proof using. introv Equiv Comp WfR Cont. sets Q: (fun x f => P x -> S x (f x)). intros x f1 f2. simpl. intros H. split. intros x' Px' Rx'x. apply~ Cont. intros y Py Ryx'. forwards~ (M1&M2&M3): (H y). rewrite rclosure_eq in Rx'x. destruct Rx'x as [Rx'x|Ex'x]. applys* tclosure_l. subst. apply~ tclosure_once. intros Px. forwards [M1 M2]: Cont f1 f1 Px. introv Py Ryx. forwards (M1&M2&M3): H y. apply~ tclosure_once. splits~. apply~ equiv_refl. apply M2. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)