Alphabet

and:[c × c] ⟶ c
arrow:[t × t] ⟶ t
lessthan:[t × t] ⟶ c

Variables

X:t
Y:t
U:t
V:t

Rules

lessthan(arrow(X, Y), arrow(U, V))⇒and(lessthan(U, X), lessthan(Y, V))