proposition: Lemma measure_wf: well_founded MR.
proof: Proof. Proof with auto. unfold well_founded. cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0). + intros H a. apply (H (m a))... + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). intros ? H ? H0. apply Acc_intro. intros y H1. unfold MR in H1. rewrite H0 in H1. apply (H (m y))... Defined.
imports: Coq.Init.Wf Coq.Program.Utils