-generalize in match (refl_eq ? (cmp d (sval d p x) (sval d p y)));
-generalize in match (cmp d (sval d p x) (sval d p y)) in ⊢ (? ? ? % → %); intros 1 (b);
-cases b; cases x (s ps); cases y (t pt); simplify; intros (Hcmp);
-[ constructor 1;
- generalize in match (eqP d s t); intros (Est);
- cases Est (H); clear Est;
- [ generalize in match ps;
- rewrite > H; intros (pt');
- rewrite < (pirrel bool (p t) true pt pt' (eqType_decidable bool_eqType));
- reflexivity;
- | cases (H (b2pT ? ? (eqP d s t) Hcmp))
- ]
-| constructor 2; unfold Not; intros (H);
- (* XXX destruct H; *)
- change in Hcmp with (cmp d (match {?,ps} with [(mk_sigma s _)⇒s]) t = false);
- rewrite > H in Hcmp; simplify in Hcmp; rewrite > cmp_refl in Hcmp; destruct Hcmp;
-]
+cases (eqP d (sval ? ? x) (sval ? ? y)); generalize in match H; clear H;
+cases x (s ps); cases y (t pt); simplify; intros (Est);
+[1: constructor 1; generalize in match ps; rewrite > Est; intros (pt');
+ rewrite < (pirrel ? ? ? pt pt' (eqType_decidable bool_eqType)); reflexivity;
+|2: constructor 2; unfold Not; intros (H); destruct H;
+ cases (Est); assumption;]