New naming policy for local variables.

[helm.git] / helm / matita / library / nat / orders.ma

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index b8e92fa2b6987f34cfecbf81841bee405d10ca0a..d4979231d1d1d46a0b4a7cea579c086fef3bdb62 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -64,7 +64,7 @@ qed.
 
 theorem le_S_S_to_le : \forall n,m:nat. le (S n) (S m) \to le n m.
 intros.change with le (pred (S n)) (pred (S m)).
-elim H.apply le_n.apply trans_le ? (pred e2).assumption.
+elim H.apply le_n.apply trans_le ? (pred n1).assumption.
 apply le_pred_n.
 qed.
 
@@ -78,7 +78,7 @@ intros.simplify.intros.apply leS_to_not_zero ? ? H.
 qed.
 
 theorem not_le_Sn_n: \forall n:nat. Not (le (S n) n).
-intros.elim n.apply not_le_Sn_O.simplify.intros.cut le (S e1) e1.
+intros.elim n.apply not_le_Sn_O.simplify.intros.cut le (S n1) n1.
 apply H.assumption.
 apply le_S_S_to_le.assumption.
 qed.