totality017.idr:19:1-15:
   |
19 | g1 T1 T1 = True
   | ~~~~~~~~~~~~~~~
Main.g1 is not total as there are missing cases

totality017.idr:25:1-17:
   |
25 | g2 T1' T1' = True
   | ~~~~~~~~~~~~~~~~~
Main.g2 is not total as there are missing cases

totality017.idr:31:1-13:
   |
31 | g3 T1' = True
   | ~~~~~~~~~~~~~
Main.g3 is not total as there are missing cases

totality017.idr:37:1-36:
   |
37 | g4 (MkTTPP (MkPP 0) (MkPP 0)) = True
   | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main.g4 is not total as there are missing cases

totality017.idr:42:1-11:
   |
42 | f' 0 = True
   | ~~~~~~~~~~~
Main.f' is not total as there are missing cases

totality017.idr:47:1-17:
   |
47 | f (MkPP 0) = True
   | ~~~~~~~~~~~~~~~~~
Main.f is not total as there are missing cases