- [ apply (λp,q. And4 (eq1 ? (or_f_minus_star_ ?? p) (or_f_minus_star_ ?? q))
- (eq1 ? (or_f_minus_ ?? p) (or_f_minus_ ?? q))
- (eq1 ? (or_f_ ?? p) (or_f_ ?? q))
- (eq1 ? (or_f_star_ ?? p) (or_f_star_ ?? q)));
- | whd; simplify; intros; repeat split; intros; apply refl1;
+ [ apply (λp,q. And4 (eq2 ? (or_f_minus_star_ ?? p) (or_f_minus_star_ ?? q))
+ (eq2 ? (or_f_minus_ ?? p) (or_f_minus_ ?? q))
+ (eq2 ? (or_f_ ?? p) (or_f_ ?? q))
+ (eq2 ? (or_f_star_ ?? p) (or_f_star_ ?? q)));
+ | whd; simplify; intros; repeat split; intros; apply refl2;