X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Ffgraph.ma;h=5b28071dcff455d2cc37d02a3f603861d05842e8;hb=59d7f64e2e1a22ded8f9017942ca640fe62d886a;hp=f4ba8abdedd71decd9eb5745d0d71aca9cbef4aa;hpb=849b36b9489da3dc3b7b4ef1a97c574f41968876;p=helm.git

diff --git a/helm/software/matita/library/decidable_kit/fgraph.ma b/helm/software/matita/library/decidable_kit/fgraph.ma
index f4ba8abde..5b28071dc 100644
--- a/helm/software/matita/library/decidable_kit/fgraph.ma
+++ b/helm/software/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.