Consider the following argument:

The present king of France is bald.

The present king of France is the present king of Alpha Centauri.

Therefore, the present king of Alpha Centauri is bald.

It seems that the argument suggested above as an example is intuitively valid one. We can construct the structure of the argument by first-order predicate logic with Russellian definite descriptions as:

(∃x)((Fx & ~(∃y)(Fy & x ≠ y)) & Gx)

(∀x)(Fx ↔ Hx)

∴ (∃x)((Hx & ~(∃y)(Hy & x ≠ y)) & Gx)

Now the question is whether we can prove the argument as valid by first-order predicate logic natural deduction such as Gentzen style of introduction and elimination rules using one, with proof method as reductio ad absurdum, or indirect derivation.