The Coq mailing list

[Pablo Argon <pargon AT cadence.com>]

Hello all,
        I want to encode a semantic function as an
inductive type.
An excerpt of my code is the following (hope is enough):

Inductive Seem  [f: (flaxpr Signal)] : nat -> Prop :=
  semTT     : (t:nat)(Sem (TTrue Signal) t)
| semFFalse : (t:nat)False -> (Sem (FFalse Signal) t)
| semnot : (t:nat) (NNot (Sem f) t)->(Sem (snot f) t)
.

Rule semnot doesn't comply with the strict positivity condition
required.
I remember that somewhere I read that we can 
transform negative occurrences into positive ones... but I can't
figure out where.

Someone can remember me the trick ?

Thank you all in advance,
        Pablo A.