To do a tableau proof of this statement: [tex](\forall x) [P(x) \vee Q(x)] \supset [(\exists x)(P(x) \vee (\exists x)(Q(x)] [/tex] I started out by restating it as follows: [tex](\forall x) [P(x) \vee Q(x)] \supset [(\exists y)(P(y) \vee (\exists z)(Q(z)] [/tex] to avoid confusion over what's bound to what (and when). Is my approach: valid? invalid? recommended? not? a good idea? not? some other adjective (or expletive)?