The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I highly doubt it. Take the substitutive equality as an example. It is defined as:

Inductive eq (A:Type) (x:A) : A -> Prop := refl : eq x x.

rather than

Inductive eq (A:Type) : A -> A -> Prop := refl (x:A) : eq x x.

They're not equivalent. The job of K is precisely to make the difference between parameters and indices moot (appart from side issues such as universes).



Arnaud

On 24 February 2012 10:08, Andrew Polonsky <andrew.polonsky AT gmail.com> wrote:

In the context

A:Type
F: A -> A
Inductive graF : A -> A -> Set := io_pair (a:A) : graF a (F a)

can one derive

forall (a:A) (g: graF a (F a)), g = io_pair a

without assuming axioms or decidability?

Thanks,
Andrew