| [ H1: (le ?1 ?2); H2: (lt ?2 (plus ?1 ?3));
H3: (TLRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
Apply (lift_gen_lref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
- | [ H: (TLRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
+ | [ _: (TLRef ?1) = (lift (S ?1) (0) ?2) |- ? ] ->
+ EApply lift_gen_lref_false; [ Idtac | Idtac | XEAuto ]; XEAuto
+ | [ H: (TLRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
LApply (lift_gen_lref_false (1) ?1 ?1); [ Intros H_x | XAuto ];
LApply H_x; [ Clear H_x; Intros H_x | Arith7' ?1; XAuto ];
LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ];