helm/coq-contribs/LAMBDA-TYPES/subst1_lift.v

   1 (*#* #stop file *)
   2
   3 Require lift_props.
   4 Require subst0_lift.
   5 Require subst1_defs.
   6
   7    Section subst1_lift. (****************************************************)
   8
   9       Theorem subst1_lift_lt : (t1,t2,u:?; i:?) (subst1 i u t1 t2) ->
  10                                (d:?) (lt i d) -> (h:?)
  11                                (subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)).
  12       Intros until 1; XElim H; Clear t2; XAuto.
  13       Qed.
  14
  15       Theorem subst1_lift_ge : (t1,t2,u:?; i,h:?) (subst1 i u t1 t2) ->
  16                                (d:?) (le d i) ->
  17                                (subst1 (plus i h) u (lift h d t1) (lift h d t2)).
  18       Intros until 1; XElim H; Clear t2; XAuto.
  19       Qed.
  20
  21    End subst1_lift.
  22
  23       Hints Resolve subst1_lift_lt subst1_lift_ge : ltlc.