X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flprs_lprs.ma;h=7421955b6e1124c38e977fc593a0fb629ee8700e;hp=ae645f6aad67c3cee61a5d1ed76ecae4108a2b3e;hb=ca7327c20c6031829fade8bb84a3a1bb66113f54;hpb=25c634037771dff0138e5e8e3d4378183ff49b86

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma
index ae645f6aa..7421955b6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma
@@ -19,10 +19,10 @@ include "basic_2/rt_computation/lprs_cpms.ma".
 
 (* Main properties **********************************************************)
 
-theorem lprs_trans (h) (G): Transitive … (lprs h G).
+theorem lprs_trans (h) (G): Transitive … (lprs h 0 G).
 /4 width=5 by lprs_cpms_trans, cprs_trans, lex_trans/ qed-.
 
-theorem lprs_conf (h) (G): confluent2 … (lprs h G) (lprs h G).
+theorem lprs_conf (h) (G): confluent2 … (lprs h 0 G) (lprs h 0 G).
 #h #G #L0 #L1 #HL01 #L2 #HL02
 elim (TC_confluent2 … L0 L1 … L2)
 [ /3 width=3 by lprs_TC, ex2_intro/ |5,6: skip