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
http://r6.ca/Goedel/goedel1.html
Require Import Eqdep_dec.
Lemma inj_right_pair2 :
∀ A : Set,
(∀ x y : A, {x = y} + {x ≠ y}) →
∀ (x : A) (P : A → Set) (y y' : P x),
existS P x y = existS P x y' → y = y'.
Lemma inj_right_pair2 :
∀ A : Set,
(∀ x y : A, {x = y} + {x ≠ y}) →
∀ (x : A) (P : A → Set) (y y' : P x),
existS P x y = existS P x y' → y = y'.
This page has been generated by coqdoc