additions in lift.ma ....

[helm.git] / matita / matita / contribs / lambda / lift.ma

diff --git a/matita/matita/contribs/lambda/lift.ma b/matita/matita/contribs/lambda/lift.ma
index 4383713e79a8a9eb133059cd0936bfcf68bfc52d..6a9b8d510976b1b144bdcde13fb01b23d92070d7 100644 (file)
--- a/matita/matita/contribs/lambda/lift.ma
+++ b/matita/matita/contribs/lambda/lift.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "trichotomy.ma".
 include "term.ma".
 
 (* RELOCATION ***************************************************************)
@@ -50,6 +49,21 @@ lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h).
 normalize // /3 width=1/
 qed.
 
+lemma lift_inv_vref_lt: ∀j,d. j < d → ∀h,M. ↑[d, h] M = #j → M = #j.
+#j #d #Hjd #h * normalize
+[ #i elim (lt_or_eq_or_gt i d) #Hid
+  [ >(tri_lt ???? … Hid) -Hid -Hjd //
+  | #H destruct >tri_eq in Hjd; #H
+    elim (plus_lt_false … H)
+  | >(tri_gt ???? … Hid)
+    lapply (transitive_lt … Hjd Hid) -Hjd -Hid #H #H0 destruct
+    elim (plus_lt_false … H)
+  ]
+| #A #H destruct
+| #B #A #H destruct
+]
+qed.
+
 lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C →
                      ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A.
 #C #d #h * normalize