proposition: Lemma mixed_contractive_as_contractive : forall I A B (M:family I B) (P:A->Prop) (F:(A->B)->(A->B)) (R:binary A) (S:I->A->B->Prop), OFE M -> wf R -> mixed_contractive M P F R S -> contractive (corec_rec_family M P R) F (fun p f => let (i,x) := p in P x -> S i x (f x)).
proof: Proof. Proof using. introv Ofe WfR Cont. sets Q: (fun p f => let (i,x) :=p:I*A in P x -> S i x (f x)). intros p f1 f2. induction_wf IH: (wf_lexico2 (ofe_wf Ofe) (wf_tclosure WfR)) p. destruct p as [i x]. intros H. split. intros j y Le Px. rewrite rclosure_eq in Le. destruct Le as [Le|Eq]. destruct (IH (j,y)) as [K _]; autos~. intros [k z] Le'. apply H. apply~ trans_lexico2. apply trans_tclosure. apply Le'. inversions Eq. forwards~ [K _]: (>> Cont i x f1 f2). intros y j Py Lt. forwards* (K1&K2&K3): (H (j,y)). forwards*: (>> rel_incl_lexico2 I A (family_r M) (family_r M) R (tclosure R) (j,y) (i,x)). introv Px. forwards~ [_ K]: (>> Cont i x f1 f2). intros y j Py Lt. forwards* (K1&K2&K3): (H (j,y)). forwards*: (>> rel_incl_lexico2 I A (family_r M) (family_r M) R (tclosure R) (j,y) (i,x)). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)