Apply H2 to the current goal.
Let v be given.
Assume H3.
Apply H3 to the current goal.
Apply SNoR_E x Hx v Hv to the current goal.
Apply HNC to the current goal.
Apply orIL to the current goal.
We use v to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv.
An exact proof term for the current goal is H3.
An exact proof term for the current goal is Hz3.