[Agda] How to solve goals that involve a vertical bar?

[Martin Stone Davis]

In the hole of the function 'put' (see code below), Agda reports that the
goal is

(get {α} {K} V {isDecEquivalence} {k₀}
>        {.Sandbox.Record.Map0WIP.recCon-NOT-PRINTED
>         (.Sandbox.Record.Map0WIP.recCon-NOT-PRINTED
>          (inj₂ (k₀ , v₀ , m₁ , k₀∉m₁)))}
>        here
>        | k₀ ≟ k₀)
>       ≡ v₀
>

I have tried invoking a with-abstraction on k₀ ≟ k₀ but to no avail: the
vertical bar remains. TIA for any help resolving this.

CODE BEGINS
    open import Level
    open import Relation.Binary.Core
    open import Data.Product
    open import Data.Sum
    open import Data.Unit.Base

    record Maybe {α} (A : Set α) : Set α where
      field
        unmaybe : ⊤ ⊎ A

    nothing : ∀ {α} {A : Set α} → Maybe A
    nothing = record { unmaybe = inj₁ tt }

    just : ∀ {α} {A : Set α} (a : A) → Maybe A
    just a = record { unmaybe = inj₂ a }

    mutual
      record Map : Set α where
        inductive
        field
          unmap : Maybe (∃ λ k₀ → V k₀ × ∃ λ m₁ → k₀ ∉ m₁)

      record _∉_ (𝑘 : K) (m₀ : Map) : Set α where
        inductive
        field
          un∉ : m₀ ≡ record { unmap = nothing } ⊎
                  ∃ λ m₁ → 𝑘 ∉ m₁ ×
                  ∃ λ k₀ → k₀ ≢ 𝑘 ×
                  ∃ λ (k₀∉m₁ : k₀ ∉ m₁) → ∃ λ v₀
                  → m₀ ≡ record { unmap = just (k₀ , v₀ , m₁ , k₀∉m₁) }

    open import Data.Empty
    open import Relation.Nullary.Negation
    open import Relation.Nullary

    _∈_ : (𝑘 : K) (m₀ : Map) → Set α
    𝑘 ∈ m₀ = ¬ 𝑘 ∉ m₀

    pattern ∅ = record { unmap = record { unmaybe = inj₁ tt } }
    pattern M⟦_+_⋆_∣_⟧ m₁ k₀ v₀ k₀∉m₁ = record { unmap = record { unmaybe =
inj₂ (k₀ , v₀ , m₁ , k₀∉m₁) } }
    pattern M⟦_+_∣_⟧ m₁ v₀ k₀∉m₁ = record { unmap = record { unmaybe = inj₂
(_ , v₀ , m₁ , k₀∉m₁) } }
    pattern M⟦_⋆_∣_⟧ k₀ v₀ k₀∉m₁ = record { unmap = record { unmaybe = inj₂
(k₀ , v₀ , _ , k₀∉m₁) } }
    pattern M⟦_∣_⟧ v₀ k₀∉m₁ = record { unmap = record { unmaybe = inj₂ (_ ,
v₀ , _ , k₀∉m₁) } }

    pattern ∉∅ = record { un∉ = (inj₁ refl) }
    pattern ¬∉∅ = record { un∉ = (inj₁ ()) }
    pattern ∉⟦_/_⟧ 𝑘∉m₁ k₀≢𝑘  = record { un∉ = inj₂ (_ , 𝑘∉m₁ , _ ,
k₀≢𝑘 , _ , _ , refl) }

    here : ∀ {k₀ : K} {v₀ : V k₀} {m₁ : Map} {k₀∉m₁ : k₀ ∉ m₁} → k₀ ∈ M⟦ v₀
∣ k₀∉m₁ ⟧
    here ¬∉∅
    here ∉⟦ _ / k₀≢k₀ ⟧ = ⊥-elim (k₀≢k₀ refl)

    infixl 40 _⊂_∣_
    _⊂_∣_ : Map → Map → (K → Set α) → Set α
    m ⊂ m' ∣ c = ∀ {𝑘} → c 𝑘 → 𝑘 ∉ m' → 𝑘 ∉ m

    shrink : ∀ {k₀ v₀ m₁ k₀∉m₁} → M⟦ m₁ + v₀ ∣ k₀∉m₁ ⟧ ⊂ m₁ ∣ λ 𝑘 → k₀ ≢ 𝑘
    shrink k₀≢𝑘 ∉∅ = ∉⟦ ∉∅ / k₀≢𝑘 ⟧
    shrink k₀≢𝑘 ∉⟦ 𝑘∉m₀ / k₁≢𝑘 ⟧ = ∉⟦ shrink k₁≢𝑘 𝑘∉m₀ / k₀≢𝑘 ⟧

    somewhere : ∀ {𝑘 k₀ v₀ m₁ k₀∉m₁} → 𝑘 ∈ M⟦ m₁ + v₀ ∣ k₀∉m₁ ⟧ → k₀ ≢ 𝑘
→ 𝑘 ∈ m₁
    somewhere 𝑘∈m₀ k₀≢𝑘 𝑘∉m₁ = contradiction (shrink k₀≢𝑘 𝑘∉m₁) 𝑘∈m₀

    open import Relation.Binary
    open import Relation.Binary.PropositionalEquality
    module _ {isDecEquivalence : IsDecEquivalence {A = K} _≡_} where
      open IsDecEquivalence isDecEquivalence using (_≟_)

      get : ∀ {𝑘 : K} {m₀ : Map} (𝑘∈m₀ : 𝑘 ∈ m₀) → V 𝑘
      get {m₀ = ∅} 𝑘∈m₀ = contradiction ∉∅ 𝑘∈m₀
      get {𝑘} {M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧} 𝑘∈m₀ with k₀ ≟ 𝑘
      get {𝑘} {M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧} 𝑘∈m₀ | yes k₀≡𝑘 rewrite k₀≡𝑘
= v₀
      get {𝑘} {M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧} 𝑘∈m₀ | no k₀≢𝑘 = get
(somewhere 𝑘∈m₀ k₀≢𝑘)

      put : (k₀ : K) → (v₀ : V k₀) (m₁ : Map) → k₀ ∉ m₁ → ∃ λ (m₀ : Map) →
∃ λ (k₀∈m₀ : k₀ ∈ m₀) → get k₀∈m₀ ≡ v₀
      put k₀ v₀ m₁ k₀∉m₁ = M⟦ m₁ + k₀ ⋆ v₀ ∣ k₀∉m₁ ⟧ , here , {!!}

CODE ENDS

--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160115/e8d51b91/attachment.html