Non dependent equality

(* NON DEPENDENT EQUALITY  *)
(* by Venanzio Capretta    *)
(* Coq version 6.2.3       *)

(* How to prove a dependend equality that doesn't depend ! *)

Section Non_Dependent_Equality.

Variable A : Set.
Variable P : A -> Prop.
Variable B : Set.

Variable f : (a:A)(P a) -> B.
Variable proof_irr : (a:A)(p1,p2 : (P a))(f a p1)=(f a p2).

(* The elimination predicate for case analysis on equality. *)
Local C : A -> A -> Prop
        := [a1,a2](p1 : (P a1))(p2 : (P a2))(f a1 p1)=(f a2 p2).

Theorem non_dep_eq : (a1, a2 : A)a1=a2 -> (C a1 a2).

End Non_Dependent_Equality.

25/02/99, 14:36