- generalize in match H6; generalize in match H7;
- cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
- apply H12; [3: apply le_S_S_to_le; assumption]
+ cases (aux n1) in H6 H7 ⊢ %; simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
+ apply H6; [3: apply le_S_S_to_le; assumption]