From 3d819f0253de734d45b2ecd2fdb96c7a049f6d32 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 31 Jul 2014 15:33:36 +0000
Subject: [PATCH] one property of abstract computation removed

---
 .../matita/contribs/lambdadelta/basic_2/computation/acp.ma  | 6 +-----
 .../contribs/lambdadelta/basic_2/computation/acp_cr.ma      | 2 +-
 .../contribs/lambdadelta/basic_2/computation/csx_lift.ma    | 1 -
 3 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma
index 59f59606b..0d054da39 100644
--- 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 e343e96f8..a7281d511 100644
--- 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 53ef87282..f81114656 100644
--- 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.
-- 
2.39.2