Let ph of type prop be given.
Assume idi_1: ph.
An exact proof term for the current goal is idi_1.
∎