- [ apply (λp,q. And42 (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)));
+ [ apply (λp,q. And42
+ (or_f_minus_star_ ?? p = or_f_minus_star_ ?? q)
+ (or_f_minus_ ?? p = or_f_minus_ ?? q)
+ (or_f_ ?? p = or_f_ ?? q)
+ (or_f_star_ ?? p = or_f_star_ ?? q));