- | subst0_bref : (v:?; i:?) (subst0 i v (TBRef i) (lift (S i) (0) v))
- | subst0_fst : (v,w,u:?; i:?) (subst0 i v u w) ->
- (t:?; k:?) (subst0 i v (TTail k u t) (TTail k w t))
- | subst0_snd : (k:?; v,w,t:?; i:?) (subst0 (s k i) v t w) -> (u:?)
- (subst0 i v (TTail k u t) (TTail k u w))
- | subst0_both : (v,u1,u2:?; i:?) (subst0 i v u1 u2) ->
- (k:?; t1,t2:?) (subst0 (s k i) v t1 t2) ->
- (subst0 i v (TTail k u1 t1) (TTail k u2 t2)).
+ | subst0_lref: (v:?; i:?) (subst0 i v (TLRef i) (lift (S i) (0) v))
+ | subst0_fst : (v,u2,u1:?; i:?) (subst0 i v u1 u2) ->
+ (t:?; k:?) (subst0 i v (TTail k u1 t) (TTail k u2 t))
+ | subst0_snd : (k:?; v,t2,t1:?; i:?) (subst0 (s k i) v t1 t2) -> (u:?)
+ (subst0 i v (TTail k u t1) (TTail k u t2))
+ | subst0_both: (v,u1,u2:?; i:?) (subst0 i v u1 u2) ->
+ (k:?; t1,t2:?) (subst0 (s k i) v t1 t2) ->
+ (subst0 i v (TTail k u1 t1) (TTail k u2 t2)).
+
+(*#* #stop file *)