Issue168b.agda

-- {-# OPTIONS -v tc.polarity:15 -v tc.inj:40 #-}
module Issue168b where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

module Membership (A : Set) where

  id : Nat → Nat
  id zero     = zero
  id (suc xs) = suc (id xs)