Issue849.agda:26,1-24
Unreachable clause
when checking the definition of f
Issue849.agda:25,1-26,11
Incomplete pattern matching for f. Missing cases:
  f .(¬ x) (d2 x)
when checking the definition of f
