Try Subst0GenBase; XAuto.
Qed.
- Theorem subst1_gen_bref : (v,x:?; i,n:?) (subst1 i v (TBRef n) x) ->
- x = (TBRef n) \/
+ Theorem subst1_gen_lref : (v,x:?; i,n:?) (subst1 i v (TLRef n) x) ->
+ x = (TLRef n) \/
n = i /\ x = (lift (S n) (0) v).
Intros; XElim H; Clear x; Intros;
Try Subst0GenBase; XAuto.