The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

On 9 janv. 2014, at 11:42, Altenkirch Thorsten 
<psztxa AT exmail.nottingham.ac.uk>
 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. So K and the wrong (because untyped)
> subterm ordering are related.

+1: All these counterexamples implicitly assume UIP on equalities of types, 
don’t they?

I’ve been wondering, in OTT adding Empty -> Box = Box would be outright 
inconsistent right? IIRC it would even actually reduce to _|_ as type 
equality is defined.

Cheers,
— Matthieu