Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* Created by Bruno Barras, Jan 1998 *)
(* Made a module instance for EqdepFacts by Hugo Herbelin, Mar 2006 *)
We prove that there is only one proof of x=x, i.e eq_refl x. This holds if the equality upon the set of x is decidable. A corollary of this theorem is the equality of the right projections of two equal dependent pairs.
Author: Thomas Kleymann |<tms@dcs.ed.ac.uk>| in Lego adapted to Coq by B. Barras
Credit: Proofs up to K_dec follow an outline by Michael Hedberg
Table of contents:
1. Streicher's K and injectivity of dependent pair hold on decidable types
1.1. Definition of the functor that builds properties of dependent equalities from a proof of decidability of equality for a set in Type
1.2. Definition of the functor that builds properties of dependent equalities from a proof of decidability of equality for a set in Set 
(************************************************************************)

Streicher's K and injectivity of dependent pair hold on decidable types

Set Implicit Arguments.
(* Set Universe Polymorphism. *)

Section EqdepDec.

  Variable A : Type.

  Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' :=
    eq_ind _ (fun a => a = y') eq2 _ eq1.

  
A:Type
comp:=fun (x y y' : A) (eq1 : x = y) (eq2 : x = y') =>
eq_ind x (fun a : A => a = y') eq2 y eq1:forall x y y' : A, x = y -> x = y' -> y = y'
forall (x y : A) (u : x = y), comp u u = eq_refl

  
A:Type
comp:=fun (x y y' : A) (eq1 : x = y) (eq2 : x = y') =>
eq_ind x (fun a : A => a = y') eq2 y eq1:forall x y y' : A, x = y -> x = y' -> y = y'
forall (x y : A) (u : x = y), comp u u = eq_refl

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x, y:A
u:x = y
comp u u = eq_refl

    case u; trivial.
  Qed.

  Variable x : A.

  Variable eq_dec : forall y:A, x = y \/ x <> y.

  Let nu (y:A) (u:x = y) : x = y :=
    match eq_dec y with
      | or_introl eqxy => eqxy
      | or_intror neqxy => False_ind _ (neqxy u)
    end.

  
A:Type
comp:=fun (x0 y y' : A) (eq1 : x0 = y) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y eq1:forall x0 y y' : A, x0 = y -> x0 = y' -> y = y'
x:A
eq_dec:forall y : A, x = y \/ x <> y
nu:=fun (y : A) (u : x = y) =>
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end:forall y : A, x = y -> x = y
forall (y : A) (u v : x = y), nu u = nu v

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u0 : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u0)
end:forall y0 : A, x = y0 -> x = y0
y:A
u, v:x = y
nu u = nu v

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u0 : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u0)
end:forall y0 : A, x = y0 -> x = y0
y:A
u, v:x = y
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end =
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy v)
end

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u0 : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u0)
end:forall y0 : A, x = y0 -> x = y0
y:A
u, v, Heq:x = y
Heq = Heq
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0)
  (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u0 : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u0)
end:forall y0 : A, x = y0 -> x = y0
y:A
u, v:x = y
Hneq:x <> y
False_ind (x = y) (Hneq u) =
False_ind (x = y) (Hneq v)

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u0 : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u0)
end:forall y0 : A, x = y0 -> x = y0
y:A
u, v, Heq:x = y
Heq = Heq
 reflexivity.

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u0 : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u0)
end:forall y0 : A, x = y0 -> x = y0
y:A
u, v:x = y
Hneq:x <> y
False_ind (x = y) (Hneq u) =
False_ind (x = y) (Hneq v)
 case Hneq; trivial.
  Qed.


  Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (eq_refl x)) v.


  
A:Type
comp:=fun (x0 y y' : A) (eq1 : x0 = y) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y eq1:forall x0 y y' : A, x0 = y -> x0 = y' -> y = y'
x:A
eq_dec:forall y : A, x = y \/ x <> y
nu:=fun (y : A) (u : x = y) =>
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end:forall y : A, x = y -> x = y
nu_constant:forall (y : A) (u v : x = y),
nu u = nu v
nu_inv:=fun (y : A) (v : x = y) => comp (nu eq_refl) v:forall y : A, x = y -> x = y
forall (y : A) (u : x = y), nu_inv (nu u) = u

  
A:Type
comp:=fun (x0 y y' : A) (eq1 : x0 = y) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y eq1:forall x0 y y' : A, x0 = y -> x0 = y' -> y = y'
x:A
eq_dec:forall y : A, x = y \/ x <> y
nu:=fun (y : A) (u : x = y) =>
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end:forall y : A, x = y -> x = y
nu_constant:forall (y : A) (u v : x = y),
nu u = nu v
nu_inv:=fun (y : A) (v : x = y) => comp (nu eq_refl) v:forall y : A, x = y -> x = y
forall (y : A) (u : x = y), nu_inv (nu u) = u

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u0 : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u0)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u0 v : x = y0),
nu u0 = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
y:A
u:x = y
nu_inv (nu u) = u

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u0 : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u0)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u0 v : x = y0),
nu u0 = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
y:A
u:x = y
comp (nu eq_refl) (nu eq_refl) = eq_refl

    apply trans_sym_eq.
  Qed.


  
A:Type
comp:=fun (x0 y y' : A) (eq1 : x0 = y) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y eq1:forall x0 y y' : A, x0 = y -> x0 = y' -> y = y'
x:A
eq_dec:forall y : A, x = y \/ x <> y
nu:=fun (y : A) (u : x = y) =>
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end:forall y : A, x = y -> x = y
nu_constant:forall (y : A) (u v : x = y),
nu u = nu v
nu_inv:=fun (y : A) (v : x = y) => comp (nu eq_refl) v:forall y : A, x = y -> x = y
forall (y : A) (p1 p2 : x = y), p1 = p2

  
A:Type
comp:=fun (x0 y y' : A) (eq1 : x0 = y) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y eq1:forall x0 y y' : A, x0 = y -> x0 = y' -> y = y'
x:A
eq_dec:forall y : A, x = y \/ x <> y
nu:=fun (y : A) (u : x = y) =>
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end:forall y : A, x = y -> x = y
nu_constant:forall (y : A) (u v : x = y),
nu u = nu v
nu_inv:=fun (y : A) (v : x = y) => comp (nu eq_refl) v:forall y : A, x = y -> x = y
forall (y : A) (p1 p2 : x = y), p1 = p2

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
y:A
p1, p2:x = y
p1 = p2

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
y:A
p1, p2:x = y
nu_inv (nu p1) = p2

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
y:A
p1, p2:x = y
nu_inv (nu p1) = nu_inv (nu p2)

    
A:Type
comp:=fun (x0 y0 y' : A) (eq1 : x0 = y0) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y0 eq1:forall x0 y0 y' : A,
x0 = y0 -> x0 = y' -> y0 = y'
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
y:A
p1, p2:x = y
nu_inv (nu p1) = nu_inv (nu p1)

    reflexivity.
  Qed.

  
A:Type
comp:=fun (x0 y y' : A) (eq1 : x0 = y) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y eq1:forall x0 y y' : A, x0 = y -> x0 = y' -> y = y'
x:A
eq_dec:forall y : A, x = y \/ x <> y
nu:=fun (y : A) (u : x = y) =>
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end:forall y : A, x = y -> x = y
nu_constant:forall (y : A) (u v : x = y),
nu u = nu v
nu_inv:=fun (y : A) (v : x = y) => comp (nu eq_refl) v:forall y : A, x = y -> x = y
forall P : x = x -> Prop,
P eq_refl -> forall p : x = x, P p

  
A:Type
comp:=fun (x0 y y' : A) (eq1 : x0 = y) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y eq1:forall x0 y y' : A, x0 = y -> x0 = y' -> y = y'
x:A
eq_dec:forall y : A, x = y \/ x <> y
nu:=fun (y : A) (u : x = y) =>
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end:forall y : A, x = y -> x = y
nu_constant:forall (y : A) (u v : x = y),
nu u = nu v
nu_inv:=fun (y : A) (v : x = y) => comp (nu eq_refl) v:forall y : A, x = y -> x = y
forall P : x = x -> Prop,
P eq_refl -> forall p : x = x, P p

    
A:Type
comp:=fun (x0 y y' : A) (eq1 : x0 = y) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y eq1:forall x0 y y' : A, x0 = y -> x0 = y' -> y = y'
x:A
eq_dec:forall y : A, x = y \/ x <> y
nu:=fun (y : A) (u : x = y) =>
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end:forall y : A, x = y -> x = y
nu_constant:forall (y : A) (u v : x = y),
nu u = nu v
nu_inv:=fun (y : A) (v : x = y) => comp (nu eq_refl) v:forall y : A, x = y -> x = y
P:x = x -> Prop
H:P eq_refl
p:x = x
P p

    
A:Type
comp:=fun (x0 y y' : A) (eq1 : x0 = y) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y eq1:forall x0 y y' : A, x0 = y -> x0 = y' -> y = y'
x:A
eq_dec:forall y : A, x = y \/ x <> y
nu:=fun (y : A) (u : x = y) =>
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end:forall y : A, x = y -> x = y
nu_constant:forall (y : A) (u v : x = y),
nu u = nu v
nu_inv:=fun (y : A) (v : x = y) => comp (nu eq_refl) v:forall y : A, x = y -> x = y
P:x = x -> Prop
H:P eq_refl
p:x = x
P eq_refl

    trivial.
  Qed.
The corollary 
  Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x :=
    match exP with
      | ex_intro _ x' prf =>
        match eq_dec x' with
          | or_introl eqprf => eq_ind x' P prf x (eq_sym eqprf)
          | _ => def
        end
    end.


  
A:Type
comp:=fun (x0 y y' : A) (eq1 : x0 = y) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y eq1:forall x0 y y' : A, x0 = y -> x0 = y' -> y = y'
x:A
eq_dec:forall y : A, x = y \/ x <> y
nu:=fun (y : A) (u : x = y) =>
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end:forall y : A, x = y -> x = y
nu_constant:forall (y : A) (u v : x = y),
nu u = nu v
nu_inv:=fun (y : A) (v : x = y) => comp (nu eq_refl) v:forall y : A, x = y -> x = y
proj:=fun (P : A -> Prop) (exP : exists y, P y)
  (def : P x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P : A -> Prop,
(exists y, P y) -> P x -> P x
forall (P : A -> Prop) (y y' : P x),
ex_intro P x y = ex_intro P x y' -> y = y'

  
A:Type
comp:=fun (x0 y y' : A) (eq1 : x0 = y) (eq2 : x0 = y') =>
eq_ind x0 (fun a : A => a = y') eq2 y eq1:forall x0 y y' : A, x0 = y -> x0 = y' -> y = y'
x:A
eq_dec:forall y : A, x = y \/ x <> y
nu:=fun (y : A) (u : x = y) =>
match eq_dec y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y) (neqxy u)
end:forall y : A, x = y -> x = y
nu_constant:forall (y : A) (u v : x = y),
nu u = nu v
nu_inv:=fun (y : A) (v : x = y) => comp (nu eq_refl) v:forall y : A, x = y -> x = y
proj:=fun (P : A -> Prop) (exP : exists y, P y)
  (def : P x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P : A -> Prop,
(exists y, P y) -> P x -> P x
forall (P : A -> Prop) (y y' : P x),
ex_intro P x y = ex_intro P x y' -> y = y'

    
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0) (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
y = y'

    
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0) (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
proj (ex_intro P x y) y = proj (ex_intro P x y') y ->
y = y'
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0)
  (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
proj (ex_intro P x y) y = proj (ex_intro P x y') y

    
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0) (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
proj (ex_intro P x y) y = proj (ex_intro P x y') y ->
y = y'
 
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0) (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
match eq_dec x with
| or_introl eqprf => eq_ind x P y x (eq_sym eqprf)
| or_intror _ => y
end =
match eq_dec x with
| or_introl eqprf => eq_ind x P y' x (eq_sym eqprf)
| or_intror _ => y
end -> y = y'

      
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0) (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
Heq:x = x
eq_ind x P y x (eq_sym Heq) =
eq_ind x P y' x (eq_sym Heq) -> y = y'
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0)
  (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
Hneq:x <> x
y = y -> y = y'

      
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0) (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
Heq:x = x
eq_ind x P y x (eq_sym Heq) =
eq_ind x P y' x (eq_sym Heq) -> y = y'
 elim Heq using K_dec_on; trivial.

      
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0) (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
Hneq:x <> x
y = y -> y = y'
 
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0) (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
Hneq:x <> x
H0:y = y
y = y'

        case Hneq; trivial.

    
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0) (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
proj (ex_intro P x y) y = proj (ex_intro P x y') y
 
A:Type
comp:=fun (x0 y0 y'0 : A) (eq1 : x0 = y0) (eq2 : x0 = y'0) =>
eq_ind x0 (fun a : A => a = y'0) eq2 y0 eq1:forall x0 y0 y'0 : A,
x0 = y0 -> x0 = y'0 -> y0 = y'0
x:A
eq_dec:forall y0 : A, x = y0 \/ x <> y0
nu:=fun (y0 : A) (u : x = y0) =>
match eq_dec y0 with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind (x = y0) (neqxy u)
end:forall y0 : A, x = y0 -> x = y0
nu_constant:forall (y0 : A) (u v : x = y0),
nu u = nu v
nu_inv:=fun (y0 : A) (v : x = y0) =>
comp (nu eq_refl) v:forall y0 : A, x = y0 -> x = y0
proj:=fun (P0 : A -> Prop) (exP : exists y, P0 y)
  (def : P0 x) =>
match exP with
| ex_intro _ x' prf =>
    match eq_dec x' with
    | or_introl eqprf =>
        eq_ind x' P0 prf x (eq_sym eqprf)
    | or_intror _ => def
    end
end:forall P0 : A -> Prop,
(exists y, P0 y) -> P0 x -> P0 x
P:A -> Prop
y, y':P x
H:ex_intro P x y = ex_intro P x y'
proj (ex_intro P x y) y = proj (ex_intro P x y) y

      reflexivity.
  Qed.

End EqdepDec.
Now we prove the versions that require decidable equality for the entire type rather than just on the given element. The rest of the file uses this total decidable equality. We could do everything using decidable equality at a point (because the induction rule for eq is really an induction rule for { y : A | x = y }), but we don't currently, because changing everything would break backward compatibility and no-one has yet taken the time to define the pointed versions, and then re-define the non-pointed versions in terms of those. 
A:Type
eq_dec:forall x0 y : A, x0 = y \/ x0 <> y
x:A
forall (y : A) (p1 p2 : x = y), p1 = p2

Proof (@eq_proofs_unicity_on A x (eq_dec x)).


A:Type
eq_dec:forall x0 y : A, x0 = y \/ x0 <> y
x:A
forall P : x = x -> Prop,
P eq_refl -> forall p : x = x, P p

Proof (@K_dec_on A x (eq_dec x)).


A:Type
eq_dec:forall x0 y : A, x0 = y \/ x0 <> y
x:A
forall (P : A -> Prop) (y y' : P x),
ex_intro P x y = ex_intro P x y' -> y = y'

Proof (@inj_right_pair_on A x (eq_dec x)).

Require Import EqdepFacts.
We deduce axiom K for (decidable) types 
forall A : Type,
(forall x y : A, {x = y} + {x <> y}) ->
forall (x : A) (P : x = x -> Prop),
P eq_refl -> forall p : x = x, P p


forall A : Type,
(forall x y : A, {x = y} + {x <> y}) ->
forall (x : A) (P : x = x -> Prop),
P eq_refl -> forall p : x = x, P p

  
A:Type
eq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
x:A
P:x = x -> Prop
H:P eq_refl
p:x = x
P p

  
A:Type
eq_dec:forall x1 y0 : A, {x1 = y0} + {x1 <> y0}
x:A
P:x = x -> Prop
H:P eq_refl
p:x = x
x0, y:A
x0 = y \/ x0 <> y
A:Type
eq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
x:A
P:x = x -> Prop
H:P eq_refl
p:x = x
P eq_refl

  
A:Type
eq_dec:forall x1 y0 : A, {x1 = y0} + {x1 <> y0}
x:A
P:x = x -> Prop
H:P eq_refl
p:x = x
x0, y:A
x0 = y \/ x0 <> y
 case (eq_dec x0 y); [left|right]; assumption.
  
A:Type
eq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
x:A
P:x = x -> Prop
H:P eq_refl
p:x = x
P eq_refl
 trivial.
Qed.


forall A : Set,
(forall x y : A, {x = y} + {x <> y}) ->
forall (x : A) (P : x = x -> Prop),
P eq_refl -> forall p : x = x, P p

Proof fun A => K_dec_type (A:=A).
We deduce the eq_rect_eq axiom for (decidable) types 
forall A : Type,
(forall x y : A, {x = y} + {x <> y}) ->
forall (p : A) (Q : A -> Type) (x : Q p) (h : p = p),
x = eq_rect p Q x p h


forall A : Type,
(forall x y : A, {x = y} + {x <> y}) ->
forall (p : A) (Q : A -> Type) (x : Q p) (h : p = p),
x = eq_rect p Q x p h

  
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (p : A) (Q : A -> Type) (x : Q p) (h : p = p),
x = eq_rect p Q x p h

  apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)).
Qed.
We deduce the injectivity of dependent equality for decidable types 
forall A : Type,
(forall x y : A, {x = y} + {x <> y}) ->
forall (P : A -> Type) (p : A) (x y : P p),
eq_dep A P p x p y -> x = y

Proof (fun A eq_dec => eq_rect_eq__eq_dep_eq A (eq_rect_eq_dec eq_dec)).


forall A : Type,
(forall x y : A, {x = y} + {x <> y}) ->
forall (x y : A) (p1 p2 : x = y), p1 = p2

Proof (fun A eq_dec => eq_dep_eq__UIP A (eq_dep_eq_dec eq_dec)).

Unset Implicit Arguments.

(************************************************************************)

Definition of the functor that builds properties of dependent equalities on decidable sets in Type

The signature of decidable sets in Type 
Module Type DecidableType.

  Monomorphic Parameter U:Type.
  Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.

End DecidableType.
The module DecidableEqDep collects equality properties for decidable set in Type 
Module DecidableEqDep (M:DecidableType).

  Import M.
Invariance by Substitution of Reflexive Equality Proofs 
  
forall (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
x = eq_rect p Q x p h

  Proof eq_rect_eq_dec eq_dec.
Injectivity of Dependent Equality 
  
forall (P : U -> Type) (p : U) (x y : P p),
eq_dep U P p x p y -> x = y

  Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq).
Uniqueness of Identity Proofs (UIP) 
  
forall (x y : U) (p1 p2 : x = y), p1 = p2

  Proof (eq_dep_eq__UIP U eq_dep_eq).
Uniqueness of Reflexive Identity Proofs 
  
forall (x : U) (p : x = x), p = eq_refl

  Proof (UIP__UIP_refl U UIP).
Streicher's axiom K 
  
forall (x : U) (P : x = x -> Prop),
P eq_refl -> forall p : x = x, P p

  Proof (K_dec_type eq_dec).
Injectivity of equality on dependent pairs in Type 
  
forall (P : U -> Type) (p : U) (x y : P p),
existT P p x = existT P p y -> x = y

  Proof eq_dep_eq__inj_pairT2 U eq_dep_eq.
Proof-irrelevance on subsets of decidable sets 
  
forall (P : U -> Prop) (x : U) (p q : P x),
ex_intro P x p = ex_intro P x q -> p = q

  
forall (P : U -> Prop) (x : U) (p q : P x),
ex_intro P x p = ex_intro P x q -> p = q

    
P:U -> Prop
x:U
p, q:P x
H:ex_intro P x p = ex_intro P x q
p = q

    
P:U -> Prop
x:U
p, q:P x
H:ex_intro P x p = ex_intro P x q
forall x0 y : U, x0 = y \/ x0 <> y
P:U -> Prop
x:U
p, q:P x
H:ex_intro P x p = ex_intro P x q
ex_intro P x p = ex_intro P x q

    
P:U -> Prop
x:U
p, q:P x
H:ex_intro P x p = ex_intro P x q
forall x0 y : U, x0 = y \/ x0 <> y
 intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption.
    
P:U -> Prop
x:U
p, q:P x
H:ex_intro P x p = ex_intro P x q
ex_intro P x p = ex_intro P x q
 assumption.
  Qed.

End DecidableEqDep.

(************************************************************************)

Definition of the functor that builds properties of dependent equalities on decidable sets in Set

The signature of decidable sets in Set 
Module Type DecidableSet.

  Parameter U:Set.
  Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.

End DecidableSet.
The module DecidableEqDepSet collects equality properties for decidable set in Set 
Module DecidableEqDepSet (M:DecidableSet).

  Import M.
  Module N:=DecidableEqDep(M).
Invariance by Substitution of Reflexive Equality Proofs 
  
forall (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
x = eq_rect p Q x p h

  Proof eq_rect_eq_dec eq_dec.
Injectivity of Dependent Equality 
  
forall (P : U -> Type) (p : U) (x y : P p),
eq_dep U P p x p y -> x = y

  Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq).
Uniqueness of Identity Proofs (UIP) 
  
forall (x y : U) (p1 p2 : x = y), p1 = p2

  Proof (eq_dep_eq__UIP U eq_dep_eq).
Uniqueness of Reflexive Identity Proofs 
  
forall (x : U) (p : x = x), p = eq_refl

  Proof (UIP__UIP_refl U UIP).
Streicher's axiom K 
  
forall (x : U) (P : x = x -> Prop),
P eq_refl -> forall p : x = x, P p

  Proof (K_dec_type eq_dec).
Proof-irrelevance on subsets of decidable sets 
  
forall (P : U -> Prop) (x : U) (p q : P x),
ex_intro P x p = ex_intro P x q -> p = q

  Proof N.inj_pairP2.
Injectivity of equality on dependent pairs in Type 
  
forall (P : U -> Type) (p : U) (x y : P p),
existT P p x = existT P p y -> x = y

  Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq.
Injectivity of equality on dependent pairs with second component in Type 
  Notation inj_pairT2 := inj_pair2.

End DecidableEqDepSet.
From decidability to inj_pair2 
forall A : Type,
(forall x y : A, {x = y} + {x <> y}) ->
forall (P : A -> Type) (p : A) (x y : P p),
existT P p x = existT P p y -> x = y


forall A : Type,
(forall x y : A, {x = y} + {x <> y}) ->
forall (P : A -> Type) (p : A) (x y : P p),
existT P p x = existT P p y -> x = y

  
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (P : A -> Type) (p : A) (x y : P p),
existT P p x = existT P p y -> x = y

  
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
Eq_dep_eq A

  
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
Eq_rect_eq A

  
A:Type
eq_dec:forall x y : A, {x = y} + {x <> y}
forall (p : A) (Q : A -> Type) (x : Q p) (h : p = p),
x = eq_rect p Q x p h

  
A:Type
eq_dec:forall x0 y : A, {x0 = y} + {x0 <> y}
p:A
Q:A -> Type
x:Q p
h:p = p
forall x0 y : A, {x0 = y} + {x0 <> y}

  apply eq_dec.
Qed.

Register inj_pair2_eq_dec as core.eqdep_dec.inj_pair2.
Examples of short direct proofs of unicity of reflexivity proofs on specific domains 
x:tt = tt
x = eq_refl


x:tt = tt
x = eq_refl

  
x:tt = tt
match tt as b return (tt = b -> Prop) with
| tt => fun x0 : tt = tt => x0 = eq_refl
end x

  destruct x; reflexivity.
Defined.


b:bool
x:b = b
x = eq_refl


b:bool
x:b = b
x = eq_refl

  
x:true = true
x = eq_refl
x:false = false
x = eq_refl

  
x:true = true
x = eq_refl
 
x:true = true
(if true as b return (true = b -> Prop)
 then fun x0 : true = true => x0 = eq_refl
 else fun _ : true = false => True) x

    destruct x; reflexivity.
  
x:false = false
x = eq_refl
 
x:false = false
(if false as b return (false = b -> Prop)
 then fun _ : false = true => True
 else fun x0 : false = false => x0 = eq_refl) x

    destruct x; reflexivity.
Defined.


n:nat
x:n = n
x = eq_refl


n:nat
x:n = n
x = eq_refl

  
x:0 = 0
x = eq_refl
n:nat
x:S n = S n
IHn:forall x0 : n = n, x0 = eq_refl
x = eq_refl

  
x:0 = 0
x = eq_refl
 
x:0 = 0
match 0 as n return (0 = n -> Prop) with
| 0 => fun x0 : 0 = 0 => x0 = eq_refl
| S n => fun _ : 0 = S n => True
end x

    destruct x; reflexivity.
  
n:nat
x:S n = S n
IHn:forall x0 : n = n, x0 = eq_refl
x = eq_refl
 
n:nat
x:S n = S n
IHn:f_equal Nat.pred x = eq_refl
x = eq_refl

    
n:nat
x:S n = S n
IHn:f_equal Nat.pred x = eq_refl
x = f_equal S eq_refl

    
n:nat
x:S n = S n
x = f_equal S (f_equal Nat.pred x)

    
n:nat
x:S n = S n
match S n as n' return (S n = n' -> Prop) with
| 0 => fun _ : S n = 0 => True
| S n' =>
    fun x0 : S n = S n' =>
    x0 = f_equal S (f_equal Nat.pred x0)
end x

  
n:nat
x:S n = S n
(fun (n0 : nat) (e : S n = n0) =>
 match n0 as n' return (S n = n' -> Prop) with
 | 0 => fun _ : S n = 0 => True
 | S n' =>
     fun x0 : S n = S n' =>
     x0 = f_equal S (f_equal Nat.pred x0)
 end e) (S n) x

  destruct x; reflexivity.
Defined.