Set Mangle Names. Goal forall (m n:nat), True. intros m n. compare m n. - constructor. - constructor. Qed.