From c9ddcf0abbb2e82eafc6dc24872244374c4f43c2 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Fri, 7 Feb 2014 18:32:54 +0100
Subject: replace rewrite with cong where feasible

---
 Bidir.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Bidir.agda')

diff --git a/Bidir.agda b/Bidir.agda
index 8998ec4..da9cafb 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -176,8 +176,8 @@ lemma->>=-just (just a) p = a , refl
 lemma->>=-just nothing  ()
 
 lemma-just-sequence : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
-lemma-just-sequence [] = refl
-lemma-just-sequence (x ∷ xs) rewrite lemma-just-sequence xs = refl
+lemma-just-sequence []       = refl
+lemma-just-sequence (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequence xs)
 
 lemma-mapM-successful : {A B : Set} {f : A → Maybe B} {n : ℕ} → (v : Vec A n) → {r : Vec B n} → mapMV f v ≡ just r → ∃ λ w → map f v ≡ map just w
 lemma-mapM-successful         []      p = [] , refl
-- 
cgit v1.2.3