Theorem no_injective_pairing : injective_pairing_statement -> ∅. Proof. intro contra. specialize (contra _ _ _ _ _ negb_weq_pair). apply toforallpaths in contra. exact (nopathstruetofalse (contra true)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.