The Coq mailing list

[Daniel Wyckoff <dwyckoff76 AT hotmail.com>]

  Dear Coq Club,
  I don't know how to prove something like the following  (without unfolding of course) (or if it's possible or what the workaround is). (Of course, I don't mind using proof irrelevance or any consistent
  axiom.) :


Variable T:Type.
Variable x y:T.
Variable P:T->Prop.
Hypothesis equal : x = y.
Variable pfx:(P x).
Variable pfy:(P y).
Definition def (a:T) (pf:(P a)) := 0 (*or whatever arbitrary defined function*).

Goal def x pfx = def y pfy.

--Daniel Wyckoff