X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Freduction%2Flpr.ma;h=0724b200737dce1ae05e5fecc481c5b74cb0615f;hp=5901ee5c0c21740eaa418e7377e8c50fec649033;hb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea;hpb=3a4509b8e569181979f5b15808361c83eb1ae49a

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2A/reduction/lpr.ma
index 5901ee5c0..0724b2007 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/reduction/lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/reduction/lpr.ma
@@ -25,11 +25,9 @@ interpretation "parallel reduction (local environment, sn variant)"
 
 (* Basic inversion lemmas ***************************************************)
 
-(* Basic_1: includes: wcpr0_gen_sort *)
 lemma lpr_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ➡ L2 → L2 = ⋆.
 /2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
 
-(* Basic_1: includes: wcpr0_gen_head *)
 lemma lpr_inv_pair1: ∀I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡ L2 →
                      ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡ K2 & ⦃G, K1⦄ ⊢ V1 ➡ V2 & L2 = K2.ⓑ{I}V2.
 /2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
@@ -55,7 +53,3 @@ lemma lpr_pair: ∀I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡ K2 → ⦃G, K1⦄ ⊢ V
 
 lemma lpr_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → |L1| = |L2|.
 /2 width=2 by lpx_sn_fwd_length/ qed-.
-
-(* Basic_1: removed theorems 3: wcpr0_getl wcpr0_getl_back
-                                pr0_subst1_back
-*)