- test.ma on the disambiguation bug moved to ONAG (just out of the way)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
index da4dd9c5acfa71ccd81206f989718917fd00265c..ba117d867f12573db855baa9ca910921ae324bd8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/notation/relations/rlift_4.ma".
 include "basic_2/grammar/term_weight.ma".
 include "basic_2/grammar/term_simple.ma".
 
@@ -20,7 +21,7 @@ include "basic_2/grammar/term_simple.ma".
 (* Basic_1: includes:
             lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
 *)
-inductive lift: nat → nat → relation term ≝
+inductive lift: relation4 nat nat term term ≝
 | lift_sort   : ∀k,d,e. lift d e (⋆k) (⋆k)
 | lift_lref_lt: ∀i,d,e. i < d → lift d e (#i) (#i)
 | lift_lref_ge: ∀i,d,e. d ≤ i → lift d e (#i) (#(i + e))
@@ -268,6 +269,22 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
+lemma lift_fwd_pair1: ∀I,T2,V1,U1,d,e. ⇧[d,e] ②{I}V1.U1 ≡ T2 →
+                      ∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & T2 = ②{I}V2.U2.
+* [ #a ] #I #T2 #V1 #U1 #d #e #H
+[ elim (lift_inv_bind1 … H) -H /2 width=4/
+|  elim (lift_inv_flat1 … H) -H /2 width=4/
+] 
+qed-.
+
+lemma lift_fwd_pair2: ∀I,T1,V2,U2,d,e. ⇧[d,e] T1 ≡ ②{I}V2.U2 →
+                      ∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & T1 = ②{I}V1.U1.
+* [ #a ] #I #T1 #V2 #U2 #d #e #H
+[ elim (lift_inv_bind2 … H) -H /2 width=4/
+|  elim (lift_inv_flat2 … H) -H /2 width=4/
+] 
+qed-.
+
 lemma lift_fwd_tw: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → ♯{T1} = ♯{T2}.
 #d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
 qed-.