1:1-1:1::Reverse.$trModule :: "GHC.Types.Module"
12:1-12:7::Reverse.length :: "x1:[a] -> {v : GHC.Types.Int | v >= 0\n                               && v == Reverse.length x1}"
13:17-13:30::lq_anf$##7205759403792797819 :: "{v : GHC.Types.Int | v == (1 : int)}"
13:19-13:20::_ :: "x1:GHC.Types.Int -> x2:GHC.Types.Int -> {v : GHC.Types.Int | v == x1 + x2}"
13:21-13:30::lq_anf$##7205759403792797820 :: "{v : GHC.Types.Int | v >= 0\n                     && v == Reverse.length xs}"
19:1-19:8::Reverse.reverse :: "x1:[a] -> {os : [a] | Reverse.length x1 == Reverse.length os}"
20:18-20:28::lq_anf$##7205759403792797824 :: "{os : [a] | Reverse.length xs == Reverse.length os\n            && os == Reverse.reverse xs}"
26:8-26:10::Reverse.++ :: "x1:[a] -> x2:[a] -> {os : [a] | Reverse.length os == Reverse.length x1 + Reverse.length x2}"
26:11-26:13::ys :: "[a]"
27:19-27:27::lq_anf$##7205759403792797822 :: "{os : [a] | Reverse.length os == Reverse.length xs + Reverse.length ys\n            && os == Reverse.++ xs ys}"
32:1-32:11::Reverse.singletonP :: "x1:a -> {VV : () | Reverse.reverse (GHC.Types.: x1 GHC.Types.[]) == GHC.Types.: x1 GHC.Types.[]}"
32:12-32:13::x :: "a"
33:7-33:18::lq_anf$##7205759403792797829 :: "[a]"
34:7-34:17::lq_anf$##7205759403792797831 :: "[a]"
35:7-35:16::lq_anf$##7205759403792797839 :: "[a]"