The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Looking about properties of John Major Equality (related to
extensional equality), we encountered the following problem.
It seems that the following property is not provable

        forall A1 A2 B1 B2 : Type,
        forall f : (A1 -> B1),
        forall g : (A2 -> B2),
        forall x1 : A1, x2:A2,
        f == g -> x1 == x2 -> (f x1) == (g x2)

== being JM equality

It is easily provably equivalent to :
        forall f : (A -> B1),
        forall g : (A -> B2),
        forall x : A,
        f == g -> (f x) == (g x)

and because the same is OK when B1=B2, this is also equivalent 
to 
        (A->B1)=(A->B2) -> A -> B1=B2 (even with Leibniz equality)

Any comment, reference on this matter will be welcome.

        Christine Paulin and Nicolas Oury
-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  tel : (+33) (0)1 69 15 66 35         fax : (+33) (0)1 69 15 65 86