From af1cc6bc8685515ffbf269e420449219a105301c Mon Sep 17 00:00:00 2001
From: Helmut Grohne <helmut@subdivi.de>
Date: Thu, 9 Feb 2012 15:08:36 +0100
Subject: prove lemma-union-generate

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

(limited to 'Bidir.agda')

diff --git a/Bidir.agda b/Bidir.agda
index 4e7d46e..332cc55 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -130,9 +130,6 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin
     ≡⟨ lemma-map-denumerate-enumerate as ⟩
   as ∎)
 
-lemma-union-generate : {A : Set} {n : ℕ} → (f : Fin n → A) → (is : List (Fin n)) → union (generate f is) (fromFunc f) ≡ fromFunc f
-lemma-union-generate f is = {!!}
-
 theorem-1 : (get : {α : Set} → List α → List α) → {τ : Set} → (eq : EqInst τ) → (s : List τ) → bff get eq s (get s) ≡ just s
 theorem-1 get eq s = begin
   bff get eq s (get s)
-- 
cgit v1.2.3