X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Facp_cr.ma;h=e8dfcbfde0612283bf67ebad19f580f1aad349a1;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=b0b15e6655d0897977405ff99ee2d109933295c8;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
index b0b15e665..e8dfcbfde 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
@@ -89,7 +89,7 @@ qed.
 lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) →
                 ∀des,L0,L,V,V0. ⇩*[des] L0 ≡ L → ⇧*[des] V ≡ V0 →
                 RP L V → RP L0 V0.
-#RR #RS #RP #HRP #des #L0 #L #V #V0 #HL0 #HV0 #HV 
+#RR #RS #RP #HRP #des #L0 #L #V #V0 #HL0 #HV0 #HV
 @acr_lifts /width=6/
 @(s7 … HRP)
 qed.
@@ -103,9 +103,9 @@ lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) →
 @conj /2 width=1/ /2 width=6 by rp_lifts/
 qed.
 
-(* Basic_1: was: 
+(* Basic_1: was:
    sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift
-*) 
+*)
 lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
                 ∀A. acr RR RS RP (aacr RP A).
 #RR #RS #RP #H1RP #H2RP #A elim A -A normalize //