proof instance : (!x:t.A(x)) & (?y:t.B(y)) => ?z:t.A(z);