- main proof for strong normalization closed! ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / unfold / lifts_lift.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma
index c10f25a300f939b9efa91d1f2617de6ba673e5b5..8bec02119c337706fd8bd16582b133ac82eaa49c 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma
@@ -29,3 +29,9 @@ lemma lifts_lift_trans_le: ∀T1,T,des. ⇧*[des] T1 ≡ T → ∀T2. ⇧[0, 1]
   elim (lift_trans_le … HT13 … HT3 ?) -T3 // /3 width=5/
 ]
 qed-.
+
+(* Basic_1: was: lift1_free (right to left) *)
+axiom lifts_lift_trans: ∀T1,T0,des0. ⇧*[des0] T1 ≡ T0 →
+                        ∀T2,i0. ⇧[O, i0 + 1] T0 ≡ T2 →
+                        ∀des,i. @[i] des ≡ i0 → des + 1 ▭ i + 1 ≡ des0 + 1 →
+                        ∃∃T. ⇧[0, i + 1] T1 ≡ T & ⇧*[des] T ≡ T2.