new implementation of the destruct tactic,

[helm.git] / matita / library / decidable_kit / fgraph.ma

diff --git a/matita/library/decidable_kit/fgraph.ma b/matita/library/decidable_kit/fgraph.ma
index f4ba8abdedd71decd9eb5745d0d71aca9cbef4aa..5b28071dcff455d2cc37d02a3f603861d05842e8 100644 (file)
--- a/matita/library/decidable_kit/fgraph.ma
+++ b/matita/library/decidable_kit/fgraph.ma
@@ -35,7 +35,7 @@ apply prove_reflect; intros;
  [1: generalize in match H; rewrite > (b2pT ? ? (eqP (list_eqType d2) ? ?) H2); 
      intros; clear H H2; rewrite < (pirrel ? ? ? H1 H3 (eqType_decidable nat_eqType));
      reflexivity
- |2: unfold Not; intros (H3); destruct H3; rewrite > Hcut in H2;
+ |2: unfold Not; intros (H3); destruct H3;
      rewrite > (cmp_refl (list_eqType d2)) in H2; destruct H2;]
 qed.