The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

On 09/01/2014 11:42, Altenkirch Thorsten wrote:
> > About K: Coq has managed to describe a pattern-match which does not
> > allow it (by making less unification information available in the
> > branches), and I don't think it's that relevant to the problem at hand,
> > which is mostly concerned about when a term is a subterm of another.
> I don't agree!
>
> If the only proof of equality is refl then it is clear that subst should
> preserve the structural ordering.

It's not clear to me. Proof-irrelevance does not mean that any equality 
admits refl as a proof!
If you apply subst with a proof of 0=1 (or, less controversially 
(False->True) = True), I see a priori no reason
why it should preserve the structural ordering. This ordering should 
remain well-founded even in inconsistent contexts.

This reasoning is sound only when you do that for proofs of x=x, and 
then yes this is obviously related to K.

Bruno.