proposition: Lemma mixed_contractive_noinv_to_mixed_contractive : forall I A B (M:family I B) (P:A->Prop) (F:(A->B)->(A->B)) (R:binary A), mixed_contractive_noinv M P F R -> mixed_contractive M P F R (fun _ => post_true).
proof: Proof. Proof using. introv Cont. unfolds. intros. split~. apply~ Cont. intros. forwards*: H0. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)