Section subst0_lift. (****************************************************)
- Theorem subst0_lift_lt : (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
- (d:?) (lt i d) -> (h:?)
- (subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)).
+ Theorem subst0_lift_lt: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
+ (d:?) (lt i d) -> (h:?)
+ (subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)).
Intros until 1; XElim H; Intros.
-(* case 1: subst0_bref *)
- Rewrite lift_bref_lt; [ Idtac | XAuto ].
+(* case 1: subst0_lref *)
+ Rewrite lift_lref_lt; [ Idtac | XAuto ].
LetTac w := (minus d (S i0)).
Arith8 d '(S i0); Rewrite lift_d; XAuto.
(* case 2: subst0_fst *)
Apply subst0_both; [ Idtac | Rewrite <- (minus_s_s k) ]; XAuto.
Qed.
- Theorem subst0_lift_ge : (t1,t2,u:?; i,h:?) (subst0 i u t1 t2) ->
- (d:?) (le d i) ->
- (subst0 (plus i h) u (lift h d t1) (lift h d t2)).
+ Theorem subst0_lift_ge: (t1,t2,u:?; i,h:?) (subst0 i u t1 t2) ->
+ (d:?) (le d i) ->
+ (subst0 (plus i h) u (lift h d t1) (lift h d t2)).
Intros until 1; XElim H; Intros.
-(* case 1: subst0_bref *)
- Rewrite lift_bref_ge; [ Idtac | XAuto ].
+(* case 1: subst0_lref *)
+ Rewrite lift_lref_ge; [ Idtac | XAuto ].
Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
Arith5'c h i0; XAuto.
(* case 2: subst0_fst *)
SRwBackIn H2; LiftTailRw; XAuto.
Qed.
- Theorem subst0_lift_ge_S : (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
- (d:?) (le d i) -> (b:?)
- (subst0 (s (Bind b) i) u (lift (1) d t1) (lift (1) d t2)).
- Intros; Simpl; Arith7 i; Apply subst0_lift_ge; XAuto.
+ Theorem subst0_lift_ge_S: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
+ (d:?) (le d i) ->
+ (subst0 (S i) u (lift (1) d t1) (lift (1) d t2)).
+ Intros; Arith7 i; Apply subst0_lift_ge; XAuto.
Qed.
- End subst0_lift.
+ Theorem subst0_lift_ge_s: (t1,t2,u:?; i:?) (subst0 i u t1 t2) ->
+ (d:?) (le d i) -> (b:?)
+ (subst0 (s (Bind b) i) u (lift (1) d t1) (lift (1) d t2)).
+ Intros; Simpl; Apply subst0_lift_ge_S; XAuto.
+ Qed.
- Hints Resolve subst0_lift_lt subst0_lift_ge subst0_lift_ge_S : ltlc.
+ End subst0_lift.
+
+ Hints Resolve subst0_lift_lt subst0_lift_ge
+ subst0_lift_ge_S subst0_lift_ge_s : ltlc.