the support for reducibility candidates evolves ,,,,

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / substitution / lift_vector.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma
index 91b03c0b9b5a1339cab8c7ecd152e6a9dab4213e..2f7c9bbc5e142cfcbe417f46968de98322035442 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma
@@ -26,3 +26,12 @@ inductive liftv (d,e:nat) : relation (list term) ≝
 
 interpretation "relocation (vector)" 'RLift d e T1s T2s = (liftv d e T1s T2s).
 
+(* Basic properties *********************************************************)
+
+lemma liftv_total: ∀d,e. ∀T1s:list term. ∃T2s. ⇑[d, e] T1s ≡ T2s.
+#d #e #T1s elim T1s -T1s
+[ /2 width=2/
+| #T1 #T1s * #T2s #HT12s
+  elim (lift_total T1 d e) /3 width=2/
+]
+qed-.