-|2: generalize in match (refl_eq ? (cmp ? x s));
- generalize in match (cmp ? x s) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
- [1: simplify; intros (Exs);
- rewrite > orbC; rewrite > H;
- [2: intros; apply H1; simplify; rewrite > H2; rewrite > orbC; reflexivity
- |1: lapply (H1 t) as H2; [2: simplify; rewrite > cmp_refl; reflexivity]
- rewrite > Hpt in H2; simplify in H2; rewrite > H2 in Exs;
- destruct Exs;]
- |2: intros (Dxs); simplify; rewrite > H;
- [2: intros; apply (H1 y); simplify; rewrite > H2; rewrite > orbC; reflexivity
- |1: rewrite > Dxs; reflexivity]]]
+|2: simplify; apply (cmpP d2 x s); simplify; intros (E);
+ [1: rewrite < (H1 a); simplify; [rewrite > Hpt; rewrite > E]
+ simplify; rewrite > cmp_refl; reflexivity
+ |2: apply H; intros; apply H1; simplify; rewrite > H2;
+ rewrite > orbC; reflexivity]]