(* case 3.1 : n < d0 *)
Rewrite minus_x_Sy in H4; [ Idtac | XAuto ].
DropGenBase; Rewrite H4 in H0; Clear H4 x.
- Rewrite lift_bref_lt; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt; [ Idtac | XAuto ].
Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
EApply ty0_abbr; XEAuto.
(* case 3.2 : n >= d0 *)
- Rewrite lift_bref_ge; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge; [ Idtac | XAuto ].
Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
Rewrite (plus_sym h (S n)); Simpl; XEAuto.
(* case 4: ty0_abst *)
(* case 4.1 : n < d0 *)
Rewrite minus_x_Sy in H4; [ Idtac | XAuto ].
DropGenBase; Rewrite H4 in H0; Clear H4 x.
- Rewrite lift_bref_lt; [ Idtac | XAuto ].
+ Rewrite lift_lref_lt; [ Idtac | XAuto ].
Arith8 d0 '(S n); Rewrite lift_d; [ Arith8' d0 '(S n) | XAuto ].
EApply ty0_abst; XEAuto.
(* case 4.2 : n >= d0 *)
- Rewrite lift_bref_ge; [ Idtac | XAuto ].
+ Rewrite lift_lref_ge; [ Idtac | XAuto ].
Arith7' n; Rewrite lift_free; [ Idtac | Simpl; XAuto | XAuto ].
Rewrite (plus_sym h (S n)); Simpl; XEAuto.
(* case 5: ty0_bind *)