On 2015-04-25 20:53, Kirill Elagin wrote: > Also note, that in Agda’s stdlib from `a ≡ b` it follows that `a` is > `b`, [...] This is not true in general for open terms. -- /NAD