update in binararies for λδ

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / reduction / lpr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2A/reduction/lpr.ma
index 5901ee5c0c21740eaa418e7377e8c50fec649033..0724b200737dce1ae05e5fecc481c5b74cb0615f 100644 (file)
--- 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
-*)