]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/tests/fguidi.ma
patched
[helm.git] / helm / matita / tests / fguidi.ma
index 77d3b44bf3715466d6ba91827f668cd51f9ab9eb..7681a7ad4e8429b17c3da11072b862eb7889ea74 100644 (file)
@@ -93,7 +93,7 @@ qed.
 
 (*
 theorem le_trans: \forall x,y. (le x y) \to \forall z. (le y z) \to (le x z).
-intros 1. elim x; clear H. (* clear x *) 
+intros 1. elim x; clear H. clear x. 
 auto.
 fwd H1 [H]. decompose H.
 *)