fact: Fixpoint even (n:nat) : Prop := match n with | O => True | S O => False | S (S n) => even n end.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat