- lambdadelta: we removed focalized reduction from snv preservation

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma
index 772cbd94a62acc7802d75a8fce6c6081e2f0e2e1..c0aff4efb56988fc79a7cb03354603d63d2d20a2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma
@@ -21,7 +21,7 @@ include "basic_2/computation/dxprs.ma".
 (* Advanced properties ******************************************************)
 
 lemma dxprs_cprs_trans: ∀h,g,L,T1,T,T2.
-                   ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+                        ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
 #h #g #L #T1 #T #T2 * #T0 #HT10 #HT0 #HT2
 lapply (cprs_trans … HT0 … HT2) -T /2 width=3/
 qed-.