-generalize in match (refl_eq nat (m q));
-generalize in match (m q) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H12:(? ? ? %); simplify in ⊢ (? ? (? ? ? % ?));
-generalize in match (refl_eq nat (m r));
-generalize in match (m r) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H14:(? ? ? %); simplify in ⊢ (? ? (? ? ? ? %));
-generalize in match (refl_eq nat (m p));
-generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X; clear X;
-intros; simplify in H16:(? ? ? %);
-apply H15; [3: apply le_n] destruct H16; destruct H14; destruct H12; clear H11 H13 H15;
+generalize in match (refl_eq nat (m p));
+generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;
+intros (H16); simplify in H16:(? ? ? %); destruct H16;
+apply H15; [3: apply le_n]