The tableaux corresponding to the two informal proofs above are given below.
Tableau to check that {[∃x.(fx)]⊃[¬(∀x.{¬[(fx)∨(gx)]})]} is valid
Tableau to check that {(∀x.{∀y.[(fx)⊃(fy)]})⊃({∀x.(fx)}∨{∀x.[¬(fx)]})} is valid
![Tableau to check that {[∃x.(fx)]⊃[¬(∀x.{¬[(fx)∨(gx)]})]} is valid](60b4c916ce17d0d8d1dbccfaef113e08e82c9b56.svg)
![Tableau to check that {(∀x.{∀y.[(fx)⊃(fy)]})⊃({∀x.(fx)}∨{∀x.[¬(fx)]})} is valid](b8e113f8ecddd48d38278373a02f9639387ad545.svg)