X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flfprs_cprs.ma;h=6eb25b37754b95ef7e80274f6e11322f1ffd7043;hb=7abd5e0412171f7d07e085d334198c034895c2c3;hp=b0f7c4a9494727ef3355cacefcd2bb4526a03c1f;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma
index b0f7c4a94..6eb25b377 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lfprs_cprs.ma
@@ -25,3 +25,6 @@ lemma lfprs_pair_dx: ∀I,L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 
 #I #L1 #L2 #HL12 #V1 #V2 #H @(cprs_ind … H) -V2
 /3 width=1/ /3 width=5/
 qed.
+(*
+lamma lfprs_cprs_conf: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L2⦄ → L1 ⊢ T1 ➡* T2 → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+*)