contribution about \lambda-\delta

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / subst1_lift.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/subst1_lift.v b/helm/coq-contribs/LAMBDA-TYPES/subst1_lift.v
new file mode 100644 (file)
index 0000000..3967571
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/subst1_lift.v
@@ -0,0 +1,23 @@
+(*#* #stop file *)
+
+Require lift_props.
+Require subst0_lift.
+Require subst1_defs.
+
+   Section subst1_lift. (****************************************************)
+
+      Theorem subst1_lift_lt : (t1,t2,u:?; i:?) (subst1 i u t1 t2) ->
+                               (d:?) (lt i d) -> (h:?)
+                               (subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)).
+      Intros until 1; XElim H; Clear t2; XAuto.
+      Qed.
+
+      Theorem subst1_lift_ge : (t1,t2,u:?; i,h:?) (subst1 i u t1 t2) ->
+                               (d:?) (le d i) ->
+                               (subst1 (plus i h) u (lift h d t1) (lift h d t2)).
+      Intros until 1; XElim H; Clear t2; XAuto.
+      Qed.
+
+   End subst1_lift.
+
+      Hints Resolve subst1_lift_lt subst1_lift_ge : ltlc.