[Agda] dependent extensionality

[Conor McBride]

Hi James

Homogeneous it may be, but...

On 29 Sep 2010, at 17:58, James Chapman wrote:

> I accidentally chopped the theorem off the bottom. Here's (hopefully)
> a more successful cut and paste...
>
> substlem : {A : Set}(P : A → Set){a a' : A}(p : a ≡ a')(x : P a) 
> (q : P
> a ≡ P a') → subst (λ x → x) q x ≡ subst P p x
> substlem P refl x refl = refl

...here be K        ^^^^

Funny business

Conor