- H3: (TBRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
- Apply (lift_gen_bref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
- | [ H: (TBRef ?1) = (lift (1) ?1 ?2) |- ? ] ->
- LApply (lift_gen_bref_false (1) ?1 ?1); [ Intros H_x | XAuto ];
+ H3: (TLRef ?2) = (lift ?3 ?1 ?4) |- ? ] ->
+ Apply (lift_gen_lref_false ?3 ?1 ?2 H1 H2 ?4 H3); XAuto
+ | [ _: (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 ];