proposition: Lemma MEASURE_def {_25210 : Type'} : (@MEASURE _25210) = (fun _8094 : _25210 -> nat => fun x : _25210 => fun y : _25210 => Peano.lt (_8094 x) (_8094 y)).
proof: Proof. exact (eq_refl (@MEASURE _25210)). Qed.
imports: coq theory_hol types