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 ];
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 ];