formulate theorem-1

1 files changed, 3 insertions, 0 deletions

diff --git a/Bidir.agda b/Bidir.agda
index e77de94..ff20caf 100644
--- a/Bidir.agda
+++ b/Bidir.agda
@@ -92,3 +92,6 @@ bff get eq s v = let s′ = idrange (length s)
                      h  = assoc eq (get s′) v
                      h′ = maybe′ (λ jh → just (union jh g)) nothing h
                  in maybe′ (λ jh′ → just (map (flip lookup jh′) s′)) nothing h′
+
+theorem-1 : (get : {α : Set} → List α → List α) → {τ : Set} → (eq : (x y : τ) → Dec (x ≡ y)) → (s : List τ) → bff get eq s (get s) ≡ just s
+theorem-1 get eq s = {!!}