Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
EApply ex3_2_intro;
- [ Rewrite lift_bref_lt | Rewrite lift_d | EApply ty0_abbr ]; XEAuto.
+ [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abbr ]; XEAuto.
(* case 3.2 : n = d0 *)
Rewrite H7; Rewrite H7 in H0; Clear H2 H7 n.
DropDis; Inversion H0; Rewrite H8 in H4; Clear H0 H7 H8 e u0.
Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
Arith4c '(0) '(minus n (1)).
EApply ex3_2_intro;
- [ Rewrite lift_bref_ge
+ [ Rewrite lift_lref_ge
| Rewrite lift_free; Simpl
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.
Pattern 3 d0; Rewrite (le_plus_minus_sym (S n) d0); [ Idtac | XAuto ].
Pattern 4 d0; Rewrite (le_plus_minus (S n) d0); [ Idtac | XAuto ].
EApply ex3_2_intro;
- [ Rewrite lift_bref_lt | Rewrite lift_d | EApply ty0_abst ]; XEAuto.
+ [ Rewrite lift_lref_lt | Rewrite lift_d | EApply ty0_abst ]; XEAuto.
(* case 4.2 : n = d0 *)
Rewrite H7; Rewrite H7 in H0; DropDis; Inversion H0.
(* case 4.3 : n > d0 *)
Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
Arith4c '(0) '(minus n (1)).
EApply ex3_2_intro;
- [ Rewrite lift_bref_ge
+ [ Rewrite lift_lref_ge
| Rewrite lift_free; Simpl
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.
LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
Rewrite <- lift_d; [ Idtac | XAuto ].
Rewrite <- le_plus_minus; [ Idtac | XAuto ].
- EApply ex3_2_intro; [ Rewrite lift_bref_lt | Idtac | EApply ty0_abbr ]; XEAuto.
+ EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abbr ]; XEAuto.
(* case 3.2 : n = d0 *)
Rewrite H6 in H0; DropDis; Inversion H0.
(* case 3.3 : n > d0 *)
Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
Arith4c '(0) '(minus n (1)).
EApply ex3_2_intro;
- [ Rewrite lift_bref_ge
+ [ Rewrite lift_lref_ge
| Rewrite lift_free; Simpl
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.
LiftGen; Rewrite <- H0 in H2; Clear H0 x2.
Rewrite <- lift_d; [ Idtac | XAuto ].
Rewrite <- le_plus_minus; [ Idtac | XAuto ].
- EApply ex3_2_intro; [ Rewrite lift_bref_lt | Idtac | EApply ty0_abst ]; XEAuto.
+ EApply ex3_2_intro; [ Rewrite lift_lref_lt | Idtac | EApply ty0_abst ]; XEAuto.
(* case 4.2 : n = d0 *)
Rewrite H6 in H0; DropDis; Inversion H0.
(* case 4.3 : n > d0 *)
Pattern 1 n; Rewrite (lt_plus_minus (0) n); [ Idtac | XEAuto ].
Arith4c '(0) '(minus n (1)).
EApply ex3_2_intro;
- [ Rewrite lift_bref_ge
+ [ Rewrite lift_lref_ge
| Rewrite lift_free; [ Simpl | Simpl | Idtac ]
| Pattern 2 n; Rewrite (minus_x_SO n)
]; XEAuto.