Give a proof or countermodel for the implicational fragment

Weich.agda

module Weich where

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

open import Decidable
open import List
  renaming (
    _∈_        to _[∈]_        ;
    _∉_        to _[∉]_        ;
    All        to All[]        ;
    Any        to Any[]        ;
    ∉→¬∈       to [∉]→¬[∈]     ;
    ¬∈→∉       to ¬[∈]→[∉]     ;
    decide∈    to decide[∈]    )
open import Ensemble

record ⊤ : Set where
  constructor trivial


postulate
  Symbol : Set
  SymbolEq : Decidable≡ Symbol

data Formula : Set where
  atom : Symbol → Formula
  _⇒_  : Formula → Formula → Formula

_≟_ : Decidable≡ (Formula)
atom x ≟ atom y with SymbolEq x y
(atom x ≟ atom .x) | yes refl = yes refl
(atom x ≟ atom y) | no neq = no φ where φ : _
                                        φ refl = neq refl
atom _ ≟ (_ ⇒ _) = no λ ()
(_ ⇒ _) ≟ atom _ = no (λ ())
(α ⇒ β) ≟ (γ ⇒ δ) with α ≟ γ
...               | no neq = no φ where φ : _
                                        φ refl = neq refl
...               | yes refl with β ≟ δ
...                          | yes refl = yes refl
...                          | no neq = no φ where φ : _
                                                   φ refl = neq refl

data Fclass : Formula → Set where
  atom   : ∀ x     → Fclass (atom x)
  simple : ∀ x β   → Fclass (atom x ⇒ β)
  leftit : ∀ α β γ → Fclass ((α ⇒ β) ⇒ γ)

fclass : (α : Formula) → Fclass α
fclass (atom x)      = atom x
fclass (atom x ⇒ β)  = simple x β
fclass ((α ⇒ β) ⇒ γ) = leftit α β γ


infix 1 _⊢_
data _⊢_ : Ensemble _≟_ → Formula → Set where
  assume     : (α : Formula)
               →                            α ∷ ∅ ⊢ α

  arrowintro : ∀{Γ β} → (α : Formula)
               →                              Γ ⊢ β
                                         --------------- ⇒⁺ α
               →                          Γ - α ⊢ α ⇒ β

  arrowelim  : ∀{Γ₁ Γ₂ α β}
               →                     Γ₁ ⊢ α ⇒ β    →    Γ₂ ⊢ α
                                    --------------------------- ⇒⁻
               →                           (Γ₁ ∪ Γ₂) ⊢ β

  close      : ∀{Γ Γ' α} → Γ ⊢ α → Γ ⊂ Γ' → Γ' ⊢ α



Reduced : {A : Set} → (xs : List (Formula)) → Set
Reduced {A} xs = All[] irreducible xs
                 where irreducible : Formula → Set
                       irreducible (atom x) = ⊤
                       irreducible (α ⇒ β) = ¬ (α [∈] xs)