- commit of the "s_computation" component ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cpxs_lreq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lreq.ma
index 4abb0b91e8939e116232320eaa3aec1d62ce7fa9..ec7a863c78b7ed1395f13eefaf6725c2e7a81f1b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lreq.ma
@@ -19,6 +19,6 @@ include "basic_2/computation/cpxs.ma".
 
 (* Properties on equivalence for local environments *************************)
 
-lemma lreq_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) (lreq 0 (∞)).
+lemma lreq_cpxs_trans: ∀h,o,G. lsub_trans … (cpxs h o G) (lreq 0 (∞)).
 /3 width=5 by lreq_cpx_trans, LTC_lsub_trans/
 qed-.