[Agda] Agda Observational equality using primUnsafeTrustMe?

[Conor McBride]

On 9 Jan 2011, at 14:44, Thorsten Altenkirch wrote:

> Ok, even if we only postulate ext : ((x: A) -> f x = g s) -> f = g  
> and add an equality ext p = refl then p may be a lie but subst (ext  
> p) reduces which can cause non-termination.

By the way, it is possible to construct a counterexample in the
manner you suggest, but in which p is not a lie.

Cheers

Conor