Closure of a hierarchy in agda

closure.agda

open import Decidable
open import List

data Arrow (A : Set) : Set where
  Atom : A → Arrow A
  _⇒_  : A → Arrow A → Arrow A

data _⊢_ {A : Set} (αs : List (Arrow A)) : Arrow A → Set where
  triv : ∀{α}   → α ∈ αs → αs ⊢ α
  elim : ∀{α β} → αs ⊢ (α ⇒ β) → αs ⊢ (Atom α) → αs ⊢ β

Arrow≟ : ∀{A} → Decidable≡ A → (x y : Arrow A) → Dec (x ≡ y)
Arrow≟ _≟_ (Atom x) (Atom y) with x ≟ y
...                          | yes refl = yes refl
...                          | no neq = no φ where φ : _
                                                   φ refl = neq refl
Arrow≟ _≟_ (Atom x) (α₂ ⇒ β₂) = no (λ ())
Arrow≟ _≟_ (α ⇒ β) (Atom x) = no (λ ())
Arrow≟ _≟_ (α ⇒ β) (γ ⇒ δ) with α ≟ γ
...                        | no neq = no φ where φ : _
                                                 φ refl = neq refl
...                        | yes refl with Arrow≟ _≟_ β δ
...                                   | yes refl = yes refl
...                                   | no neq = no φ where φ : _
                                                            φ refl = neq refl

inClosure : ∀{A} → Decidable≡ A
            → (α : Arrow A) → (αs : List (Arrow A)) → Dec (αs ⊢ α)
inClosure _≟_ α αs with decide∈ (Arrow≟ _≟_) α αs
inClosure _≟_ α αs | yes pf = yes (triv pf)
inClosure _≟_ α αs | no npf = {!   !}