Bind Rule uses Existential Quantifier

This benchmark:

uf.650702.smt2 (careful it is big, if I ever find a smaller one I'll update this issue)

Run with options --proof=- --proof-define-skolems --proof-prune --proof-merge Has a bind subproof in it:

(anchor :step t12.t1 :args ((veriT_vr136 S5) (veriT_vr137 S5) (veriT_vr138 S2) (:= (veriT_vr135 S5) veriT_vr136) (:= (veriT_vr136 S5) veriT_vr137) (:= (veriT_vr133 S2) veriT_vr138)))
...
(step t12.t1.t23 (cl (= (and (= veriT_vr132 (f13 (f14 (f15 f16 f12) (f10 (f11 f12 (f10 f17 veriT_vr135)) veriT_vr136)) veriT_vr133)) (= f1 (f6 f9 (f13 (f14 (f15 f16 f12) (f21 (f24 (f25 f26 veriT_vr135) veriT_vr136) f27)) veriT_vr133))) (= f1 (f6 f9 veriT_vr136))) (and (= veriT_vr132 (f13 (f14 (f15 f16 f12) (f10 (f11 f12 (f10 f17 veriT_vr136)) veriT_vr137)) veriT_vr138)) (= f1 (f6 f9 (f13 (f14 (f15 f16 f12) (f21 (f24 (f25 f26 veriT_vr136) veriT_vr137) f27)) veriT_vr138))) (= f1 (f6 f9 veriT_vr137))))) :rule cong :premises (t12.t1.t9 t12.t1.t19 t12.t1.t22))
(step t12.t1 (cl (= (exists ((veriT_vr135 S5) (veriT_vr136 S5) (veriT_vr133 S2)) (and (= veriT_vr132 (f13 (f14 (f15 f16 f12) (f10 (f11 f12 (f10 f17 veriT_vr135)) veriT_vr136)) veriT_vr133)) (= f1 (f6 f9 (f13 (f14 (f15 f16 f12) (f21 (f24 (f25 f26 veriT_vr135) veriT_vr136) f27)) veriT_vr133))) (= f1 (f6 f9 veriT_vr136)))) (exists ((veriT_vr136 S5) (veriT_vr137 S5) (veriT_vr138 S2)) (and (= veriT_vr132 (f13 (f14 (f15 f16 f12) (f10 (f11 f12 (f10 f17 veriT_vr136)) veriT_vr137)) veriT_vr138)) (= f1 (f6 f9 (f13 (f14 (f15 f16 f12) (f21 (f24 (f25 f26 veriT_vr136) veriT_vr137) f27)) veriT_vr138))) (= f1 (f6 f9 veriT_vr137)))))) :rule bind)

That seems to add existential quantifiers instead of universal ones (which the standard requires)!