The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

Let's say we have a definition such as the following (which require
the --impredicative-set argument):

   Inductive Foo : Set :=
      | toto : forall k:Set, (k -> nat) -> Foo
      | ...

Given a proof that "toto K1 F1 = toto K2 F2", we cannot prove that "K1 =
K2" because that would require a strong elimination on a large
inductive type.

Has there been any work that would (tend to) show under which circumstances
adding an axiom as below preserves or breaks soundness?

  Axiom Eq_toto : forall (K1 K2:Set) F1 F2 P,
                  toto K1 F1 = toto K2 F2 -> P K1 F1 -> P K2 F2.


-- Stefan