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