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