[Agda] Stymied by a proof irrelevance requirement

[Jacques Carette]

On 13-04-01 09:07 PM, Wolfram Kahl wrote:
> You need a dependent variant of cong₂ that is ``missing'' from
> Relation.Binary.PropositionalEquality:
>
> cong₂D  :  {a b c : Level} {A : Set a} {B : A → Set b} {C : Set c} (f : (x : A) → B x → C)
>            →  {x₁ x₂ : A} {y₁ : B x₁} {y₂ : B x₂}
>            →  (x₁≡x₂ : x₁ ≡ x₂) → y₁ ≡ subst B (sym x₁≡x₂) y₂ → f x₁ y₁ ≡ f x₂ y₂
> cong₂D f refl refl = refl

Thanks Wolfram, that was indeed exactly what I needed.  I had knew I had 
to use a variant of cong₂ here, as well as proof-irrelevance, but this 
exact use of 'subst' may well have eluded me for quite some time.

Also, might it be a good idea to "upgrade" the standard library's cong₂ 
to this dependent version?

Jacques