From ab5bd5693f85750462418566e0310cb42a6cf6b0 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Thu, 9 Feb 2012 15:33:38 +0100
Subject: formulate theorem-2

---
 Bidir.agda | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'Bidir.agda')

diff --git a/Bidir.agda b/Bidir.agda
index 332cc55..23381d0 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -151,3 +151,6 @@ theorem-1 get eq s = begin
   just (map (denumerate s) (enumerate s))
     ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩
   just s ∎
+
+theorem-2 : (get : {α : Set} → List α → List α) → {τ : Set} → (eq : EqInst τ) → (v s u : List τ) → bff get eq s v ≡ just u → get u ≡ v
+theorem-2 get eq v s u p = {!!}
-- 
cgit v1.2.3