Add definitional Proof-Irrelevance