Proposition Extensionality

Proposition extensionality states that for propositions $P,Q:\mathrm{Prop}$, then $P\leftrightarrow Q⟹P=Q$.