Let X, T' and T be given.

Apply iffI to the current goal.

Assume H.

An exact proof term for the current goal is H.

Assume H.

An exact proof term for the current goal is H.

∎