[1,2:apply H8;
|3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
simplify in ⊢ (?→? (? % ?) ?→?);
intros; lapply (H5 i j) as H14;
[2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
[1,2:apply H8;
|3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
simplify in ⊢ (?→? (? % ?) ?→?);
intros; lapply (H5 i j) as H14;
[2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]