fact: Definition Filter filter s := let '(x:::s') := s in let s'' := filter s' in If P x then x:::s'' else s''.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat