proposition: Lemma contractive_noinv_to_contractive : forall I A (M:family I A) (F:A->A), contractive_noinv M F -> contractive M F (fun _ _ => True).
proof: Proof. Proof using. introv Cont. unfolds. intros. split~. apply Cont. intros. forwards*: H. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)