std-lib should have cong-app

[UlfNorell]

From andreas....@gmail.com on November 18, 2013 11:32:58

Patch attached, contains the two functions below, which we use very frequently.

hunk ./src/Relation/Binary/HeterogeneousEquality.agda 75

+cong-app : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →

• f ≅ g → (x : A) → f x ≅ g x +cong-app refl x = refl

hunk ./src/Relation/Binary/PropositionalEquality.agda 35

+cong-app : ∀ {a b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →

• f ≡ g → (x : A) → f x ≡ g x +cong-app refl x = refl

Attachment: cong-app.patch

Original issue: http://code.google.com/p/agda/issues/detail?id=968