alphaorder : term -> term -> int
# alphaorder `x + 1` `p ==> q`;; val it : int = -1 # alphaorder `p ==> q` `x + 1`;; val it : int = 1
# alphaorder `!x. ?y. x + 1 < y` `!y. ?z. y + 1 < z`;; val it : int = 0 # alphaorder `!x. ?y. x + 1 < y` `!x. ?y. x + 1 < y + 1`;; val it : int = -1