Let X, Tx, net and x be given.

Assume H: net_converges X Tx net x.

An exact proof term for the current goal is H.

∎