X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fdecidable_kit%2Ffgraph.ma;h=5b28071dcff455d2cc37d02a3f603861d05842e8;hb=ef870606391fff198f215127eb022eb3e41ab1d4;hp=f4ba8abdedd71decd9eb5745d0d71aca9cbef4aa;hpb=040b70279b9bf0f576f00a9b1ad28df3c8bf6024;p=helm.git

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