- 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.