λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / lprs_ctc.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_ctc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_ctc.ma
index 742a0038ae51cea23edcfed2dc832b8adfd7dd1e..c3e72888bb0996373d49d7cbe6d50456adacd33c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_ctc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_ctc.ma
@@ -20,7 +20,7 @@ include "basic_2/rt_computation/lprs.ma".
 (* Properties with contextual transitive closure ****************************)
 
 lemma lprs_CTC (h) (G):
-               ∀L1,L2. L1⪤[CTC … (λL. cpm h G L 0)] L2 → ⦃G,L1⦄⊢ ➡*[h] L2. 
+               ∀L1,L2. L1⪤[CTC … (λL. cpm h G L 0)] L2 → ⦃G,L1⦄⊢ ➡*[h] L2.
 /3 width=3 by cprs_CTC, lex_co/ qed.
 
 (* Inversion lemmas with contextual transitive closure **********************)