-generalize in match (refl_eq ? (cmp d e s1)); generalize in match (cmp d e s1) in ⊢ (? ? ? % → %);
-intros 1 (b); cases b; clear b; intros (E); cases (lcmp d l1 hd);
-[1,2: rewrite > (b2pT ? ? (eqP ? ? ?) E); simplify; rewrite > cmp_refl; reflexivity
-|3,4: rewrite > andbC; simplify; [2: reflexivity] rewrite > orbC;
- simplify; apply (p2bF ? ? (eqP ? ? ?)); unfold Not; intros (H); rewrite > H in E;
- rewrite > cmp_refl in E; destruct E;]
+apply (cmpP ? e s1); cases (lcmp d l1 hd); intros (E);
+[1,2: rewrite > E; simplify; rewrite > cmp_refl; reflexivity
+|3,4: rewrite > cmpC; rewrite > E; simplify; reflexivity;]