- drop_main: bug fix

[helm.git] / matita / matita / lib / lambda-delta / substitution / drop_main.ma

diff --git a/matita/matita/lib/lambda-delta/substitution/drop_main.ma b/matita/matita/lib/lambda-delta/substitution/drop_main.ma
index f456b9e07b3ab3aee3685441b2250388aee7d425..dc6f00d405a88e7c1cb304546c0e37f445f9cada 100644 (file)
--- 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 →