[Agda] I'm not sure... case for the constructor ..., because I get stuck when trying to solve...

[flicky frans]

Here is one another option:

open import Data.Bool
open import Relation.Binary.PropositionalEquality

data Term : Bool → Set where
  I : Term false
  App : (a b : Bool) → Term a → Term b → Term (a ∨ b)

test' : ∀ {a} → a ≡ false → Term a → Set
test' p   I                      = Bool
test' p  (App false false t1 t2) = Bool
test' () (App false true  t1 t2)
test' () (App true  b     t1 t2)

test : Term false → Set
test = test' refl