more discriminate

[helm.git] / helm / software / matita / library / decidable_kit / eqtype.ma

diff --git a/helm/software/matita/library/decidable_kit/eqtype.ma b/helm/software/matita/library/decidable_kit/eqtype.ma
index 7b0f94ed49e2ef89ce94ad64cac4ac65d6938940..ae0b075415bfc1a285f513246810cdb0edd68b57 100644 (file)
--- a/helm/software/matita/library/decidable_kit/eqtype.ma
+++ b/helm/software/matita/library/decidable_kit/eqtype.ma
@@ -102,11 +102,8 @@ cases b; cases x (s ps); cases y (t pt); simplify; intros (Hcmp);
     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;
-]
+| constructor 2; unfold Not; intros (H); destruct H; 
+  rewrite > Hcut in Hcmp; rewrite > cmp_refl in Hcmp; destruct Hcmp;] 
 qed. 
 
 definition sub_eqType ≝ λd : eqType.λp. mk_eqType ? ? (sigma_eq_dec d p).
@@ -138,20 +135,14 @@ generalize in match (refl_eq ? (ocmp ? a b));
 generalize in match (ocmp ? a b) in ⊢ (? ? ? % → %); intros 1 (c);
 cases c; intros (H); [ apply reflect_true | apply reflect_false ];
 generalize in match H; clear H;
-cases a; cases b;
-[1: intros; reflexivity;
-|2,3: intros (H); destruct H;
-|4: intros (H); simplify in H; rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity; 
-    (* se faccio la rewrite diretta non tipa *)
-|5: intros (H H1); destruct H
-|6,7: unfold Not; intros (H H1); destruct H1
-|8: unfold Not; simplify; intros (H H1); 
-    (* ancora injection non va *)
-    cut (s = s1); [ rewrite > Hcut in H;  rewrite > cmp_refl in H;  destruct H;].
-    change with (match (Some d s) with
-                 [ None ⇒ s | (Some s) ⇒ s] = s1); rewrite > H1;
-                 simplify; reflexivity;
-] qed.
+cases a; cases b; simplify; intros (H);
+[1: reflexivity;
+|2,3,5: destruct H;
+|4: rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity; 
+|6,7: unfold Not; intros (H1); destruct H1
+|8: unfold Not; intros (H1); destruct H1; 
+    rewrite > Hcut in H;  rewrite > cmp_refl in H; destruct H;]
+qed.
 
 definition option_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (ocmpP d).
 definition option_canonical_eqType : ∀d:eqType.d → option_eqType d ≝