module exampleCaseDistinctionComplexExpression where


data ⊤ : Set where
  true : ⊤


data ⊥ : Set where


data Bool : Set where
  tt : Bool
  ff : Bool

Atom : Bool -> Set
Atom ff = ⊥ 
Atom tt = ⊤

_∧Bool_ : Bool -> Bool -> Bool
ff ∧Bool _ = ff
tt ∧Bool b = b



record ProdBool : Set where
  field
    fst : Bool
    snd : Bool

f : (p : ProdBool) -> Atom ((ProdBool.fst p) ∧Bool (ProdBool.snd p))
f p = {! !}