- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / xprs_cprs.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma
index 0d2e22c58f1e289cbc0f1c4da13a070098286f30..13a4f88897bf4235b90c2888f985b48c81a801e1 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma
@@ -19,7 +19,6 @@ include "basic_2/computation/xprs.ma".
 
 (* properties on context sensitive parallel computation for terms ***********)
 
-lemma cprs_xprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2.
-#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 //
-/3 width=3 by xprs_strap1, cpr_xpr/ (**) (* NTypeChecker failure without trace *)
+lemma cprs_xprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 •➡*[g] T2.
+#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/
 qed.