Why is the type ∀t.t un-inhabited in System F? Posted by Apoorv, at cs.stackexchange.com, 20 Jan 2020 How do you prove that there exists no term with the type $\forall t. t$ in System F? I tried searching through Pierce's TAPL…