path: root/examples/tutch/support/hw3_6c.req

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