one property of abstract computation removed

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma
index 59f59606b151fb023d54dec3ffbfa21bca87f362..0d054da39e51417de00ed28354993be77101fbf2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma
@@ -32,15 +32,11 @@ definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
 definition CP2 ≝ λRP:relation3 genv lenv term.
                  ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T.
 
-definition CP3 ≝ λRP:relation3 genv lenv term.
-                 ∀G,L,W,T. RP G L W → RP G L T → RP G L (ⓝW.T).
-
 (* requirements for abstract computation properties *)
 record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:relation3 genv lenv term) : Prop ≝
 { cp0: CP0 RR RS;
   cp1: CP1 RR RS;
-  cp2: CP2 RP;
-  cp3: CP3 RP
+  cp2: CP2 RP
 }.
 
 (* Basic properties *********************************************************)

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 e343e96f89c638236acf9da269bae82eb5f78809..a7281d51185c0e639f54265e94997536636e9438 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma
@@ -182,7 +182,7 @@ lapply (acr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0
 @(s6 … HCA … (◊) (◊)) //
 [ @(HA … HL0) //
 | lapply (s1 … HCB) -HCB #HCB
-  @(cp3 … H1RP) /2 width=1 by/
+  @(s7 … H2RP … (◊)) /2 width=1 by/
 ]
 qed.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
index 53ef87282798fba2dadc371b80a2e81c616f7782..f8111465638dc8ffca685fdeb2d6f260b34d519a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
@@ -114,6 +114,5 @@ theorem csx_acp: ∀h,g. acp (cpx h g) (eq …) (csx h g).
 [ /3 width=13 by cnx_lift/
 | #G #L elim (deg_total h g 0) /3 width=8 by cnx_sort_iter, ex_intro/
 | /2 width=3 by csx_fwd_flat_dx/
-| /2 width=1 by csx_cast/
 ]
 qed.