X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda-delta%2Fsubstitution%2Fdrop_main.ma;h=dc6f00d405a88e7c1cb304546c0e37f445f9cada;hb=6b7c050f991cf7ed33bbceb0b3cdc530647eb261;hp=f456b9e07b3ab3aee3685441b2250388aee7d425;hpb=2912d9bd61bc451c1135ca0a123cc30f203e93c9;p=helm.git

diff --git a/matita/matita/lib/lambda-delta/substitution/drop_main.ma b/matita/matita/lib/lambda-delta/substitution/drop_main.ma
index f456b9e07..dc6f00d40 100644
--- a/matita/matita/lib/lambda-delta/substitution/drop_main.ma
+++ b/matita/matita/lib/lambda-delta/substitution/drop_main.ma
@@ -21,12 +21,13 @@ include "lambda-delta/substitution/drop_defs.ma".
 axiom drop_conf_ge: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
                     ∀e2,L2. ↑[0, e2] L2 ≡ L → d1 + e1 ≤ e2 →
                     ↑[0, e2 - e1] L2 ≡ L1.
+      
 
 axiom drop_conf_lt: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
                     ∀e2,K2,I,V2. ↑[0, e2] K2. 𝕓{I} V2 ≡ L →
                     e2 < d1 → let d ≝ d1 - e2 - 1 in
                     ∃∃K1,V1. ↑[0, e2] K1. 𝕓{I} V1 ≡ L1 & 
-                             ↑[d, e1] K2 ≡ K1 & ↑[d,e1] V1 ≡ V2.
+                             ↑[d, e1] K1 ≡ K2 & ↑[d,e1] V1 ≡ V2.
 
 axiom drop_trans_le: ∀d1,e1,L1. ∀L:lenv. ↑[d1, e1] L ≡ L1 →
                      ∀e2,L2. ↑[0, e2] L2 ≡ L → e2 ≤ d1 →