Library pairing.misc

This code is part of Russell O'Connor's formalisation of Goedel's Incompleteness Theorem in Coq, released into the Public Domain.

http://r6.ca/Goedel/goedel1.html
Require Import Eqdep_dec.

Lemma inj_right_pair2 :
 ∀ A : Set,
 (∀ x y : A, {x = y} + {xy}) →
 ∀ (x : A) (P : ASet) (y y' : P x),
 existS P x y = existS P x y'y = y'.

This page has been generated by coqdoc