Propositions As Types : 1

One of my favorite mathematical tricks — it seems almost too tricky to be true — is the Propositions As Types Analogy.  And I see hints the 2-part analogy can be extended to a 3-part analogy, as follows.

$\text{proof hint : proof : proposition ~:~:~ untyped term : typed term : type}$