proof frobenius : (R & ?x:t.Q(x)) <=> ?x:t.(R & Q(x));