X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Feqtype.ma;h=ae0b075415bfc1a285f513246810cdb0edd68b57;hb=99de9c457e6aaac40a64a44433d6163ad0d17263;hp=7b0f94ed49e2ef89ce94ad64cac4ac65d6938940;hpb=680039d60c1d69521f84580ee0069cb2d6ff56ba;p=helm.git

diff --git a/helm/software/matita/library/decidable_kit/eqtype.ma b/helm/software/matita/library/decidable_kit/eqtype.ma
index 7b0f94ed4..ae0b07541 100644
--- 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 ≝