Prova simbólica de teoremas Haskell usando solução SMT
