6 Section subst0_lift. (****************************************************)
8 Theorem subst0_lift_lt: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
9 (d:?) (lt i d) -> (h:?)
10 (subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)).
11 Intros until 1; XElim H; Intros.
12 (* case 1: subst0_lref *)
13 Rewrite lift_lref_lt; [ Idtac | XAuto ].
14 LetTac w := (minus d (S i0)).
15 Arith8 d '(S i0); Rewrite lift_d; XAuto.
16 (* case 2: subst0_fst *)
18 (* case 3: subst0_snd *)
19 SRwBackIn H0; LiftTailRw; Rewrite <- (minus_s_s k); XAuto.
20 (* case 4: subst0_both *)
21 SRwBackIn H2; LiftTailRw.
22 Apply subst0_both; [ Idtac | Rewrite <- (minus_s_s k) ]; XAuto.
25 Theorem subst0_lift_ge: (t1,t2,u:?; i,h:?) (subst0 i u t1 t2) ->
27 (subst0 (plus i h) u (lift h d t1) (lift h d t2)).
28 Intros until 1; XElim H; Intros.
29 (* case 1: subst0_lref *)
30 Rewrite lift_lref_ge; [ Idtac | XAuto ].
31 Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
33 (* case 2: subst0_fst *)
35 (* case 3: subst0_snd *)
36 SRwBackIn H0; LiftTailRw; XAuto.
37 (* case 4: subst0_snd *)
38 SRwBackIn H2; LiftTailRw; XAuto.
41 Theorem subst0_lift_ge_S: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
43 (subst0 (S i) u (lift (1) d t1) (lift (1) d t2)).
44 Intros; Arith7 i; Apply subst0_lift_ge; XAuto.
47 Theorem subst0_lift_ge_s: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
48 (d:?) (le d i) -> (b:?)
49 (subst0 (s (Bind b) i) u (lift (1) d t1) (lift (1) d t2)).
50 Intros; Simpl; Apply subst0_lift_ge_S; XAuto.
55 Hints Resolve subst0_lift_lt subst0_lift_ge
56 subst0_lift_ge_S subst0_lift_ge_s : ltlc.