Let 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.

∎