totality016.idr:15:1-21:
   |
15 | f1 (MkTP T1 x) = True
   | ~~~~~~~~~~~~~~~~~~~~~
Main.f1 is not total as there are missing cases

totality016.idr:19:1-24:
   |
19 | f2 (MkTP T1 x, _) = True
   | ~~~~~~~~~~~~~~~~~~~~~~~~
Main.f2 is not total as there are missing cases

totality016.idr:23:1-29:
   |
23 | f3 ((MkTP T1 x, _), _) = True
   | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main.f3 is not total as there are missing cases

totality016.idr:27:1-14:
   |
27 | g1 T1 x = True
   | ~~~~~~~~~~~~~~
Main.g1 is not total as there are missing cases

totality016.idr:31:1-17:
   |
31 | g2 (T1, x) = True
   | ~~~~~~~~~~~~~~~~~
Main.g2 is not total as there are missing cases

totality016.idr:35:1-16:
   |
35 | h1 True x = True
   | ~~~~~~~~~~~~~~~~
Main.h1 is not total as there are missing cases

totality016.idr:39:1-19:
   |
39 | h2 (True, x) = True
   | ~~~~~~~~~~~~~~~~~~~
Main.h2 is not total as there are missing cases

totality016.idr:43:1-25:
   |
43 | h3 (MkTP2 (T1, x)) = True
   | ~~~~~~~~~~~~~~~~~~~~~~~~~
Main.h3 is not total as there are missing cases

totality016.idr:47:1-30:
   |
47 | h4 (MkTP2 (T1, x), _) _ = True
   | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main.h4 is not total as there are missing cases