// problem file "fol2a.txt"
type T;
pred p(x:T,y:T);
theorem T ⇔ (∃x:T.∀y:T.p(x,y)) ⇒ (∀x:T.∃y:T.p(y,x));
