clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
generalize in match (refl_eq nat (m p));
generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;
clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
generalize in match (refl_eq nat (m p));
generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;