advances on csx towards strong normalization of rt-computation ,,,

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
index afb3e127a6a9b65c02dcd0afe41e0835cb80f1f0..6f0cef9d0be252cf2e58847e28a0d538b1b36101 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
@@ -49,6 +49,14 @@ definition deliftable2_sn: predicate (relation term) ≝
                            λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≡ U1 →
                            ∃∃T2. ⬆*[f] T2 ≡ U2 & R T1 T2.
 
+definition liftable2_bi: predicate (relation term) ≝
+                         λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≡ U1 → 
+                         ∀U2. ⬆*[f] T2 ≡ U2 → R U1 U2.
+
+definition deliftable2_bi: predicate (relation term) ≝
+                           λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≡ U1 →
+                           ∀T2. ⬆*[f] T2 ≡ U2 → R T1 T2.
+
 (* Basic inversion lemmas ***************************************************)
 
 fact lifts_inv_sort1_aux: ∀f,X,Y. ⬆*[f] X ≡ Y → ∀s. X = ⋆s → Y = ⋆s.