Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
Rewrite (plus_sym h (S n)); Simpl; XEAuto.
(* case 4: ty0_abst *)
Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
Rewrite (plus_sym h (S n)); Simpl; XEAuto.
(* case 4: ty0_abst *)