Issue168.agda

{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.polarity:10 -v tc.inj:40 -v tc.conv.irr:20 #-}  -- -v tc.mod.apply:100 #-}
module Issue168 where

postulate X : Set

open import Issue168b
open Membership X

postulate
  P : Nat → Set
  lemma : ∀ n → P (id n)

foo : P zero
foo = lemma _