MESON[]

`((?x. !y. P(x) <=> P(y)) <=> ((?x. Q(x)) <=> (!y. Q(y)))) <=>

((?x. !y. Q(x) <=> Q(y)) <=> ((?x. P(x)) <=> (!y. P(y))))`;;

MESON[]

`(!x y z. P x y /\ P y z ==> P x z) /\

(!x y z. Q x y /\ Q y z ==> Q x z) /\

(!x y. P x y ==> P y x) /\

(!x y. P x y \/ Q x y)

==> (!x y. P x y) \/ (!x y. Q x y)`;;

let ewd1062 = MESON[]

`(!x. x <= x) /\

(!x y z. x <= y /\ y <= z ==> x <= z) /\

(!x y. f(x) <= y <=> x <= g(y))

==> (!x y. x <= y ==> f(x) <= f(y)) /\

(!x y. x <= y ==> g(x) <= g(y))`;;

let ewd1062 = MESON[]

`(!x. R x x) /\

(!x y z. R x y /\ R y z ==> R x z) /\

(!x y. R (f x) y <=> R x (g y))

==> (!x y. R x y ==> R (f x) (f y)) /\

(!x y. R x y ==> R (g x) (g y))`;;

MESON[] `(?!x. g(f x) = x) <=> (?!y. f(g y) = y)`;;

MESON [ADD_ASSOC; ADD_SYM] `m + (n + p) = n + (m + p)`;;