proposition: Lemma wf_MR {A R} `(WellFounded A R) {B} (f : B -> A) : WellFounded (MR R f).
proof: Proof. red. apply measure_wf. apply H. Defined.
imports: Coq(Wf_nat Relations) Coq(Wellfounded Relation_Definitions) Coq(Relation_Operators Lexicographic_Product Wf_nat) Equations(Init Signature) Equations.CoreTactics Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.DepElim Equations.Prop.Constants