X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpaths%2Falternative_standard_order.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda%2Fpaths%2Falternative_standard_order.ma;h=e8eca4f11e88a217f1e7550bdca125344ea3be93;hb=81fc94f4f091ec35d41e2711207218d255b75273;hp=144c1dabfde927924019c95859eaa5a0bda90b46;hpb=39aab7babf51252cecb81a66af82fe797e8dcbe7;p=helm.git

diff --git a/matita/matita/contribs/lambda/paths/alternative_standard_order.ma b/matita/matita/contribs/lambda/paths/alternative_standard_order.ma
index 144c1dabf..e8eca4f11 100644
--- a/matita/matita/contribs/lambda/paths/alternative_standard_order.ma
+++ b/matita/matita/contribs/lambda/paths/alternative_standard_order.ma
@@ -26,7 +26,7 @@ lemma slt_step_rc: ∀p,q. p ≺ q → p < q.
 /2 width=1/
 qed.
 
-lemma slt_nil: ∀c,p. ◊ < c::p.
+lemma slt_nil: ∀o,p. ◊ < o::p.
 /2 width=1/
 qed.
 
@@ -34,8 +34,8 @@ lemma slt_skip: dx::◊ < ◊.
 /2 width=1/
 qed.
 
-lemma slt_comp: ∀c,p,q. p < q → c::p < c::q.
-#c #p #q #H elim H -q /3 width=1/ /3 width=3/
+lemma slt_comp: ∀o,p,q. p < q → o::p < o::q.
+#o #p #q #H elim H -q /3 width=1/ /3 width=3/
 qed.
 
 theorem slt_trans: transitive … slt.