(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 8 0) (UN Unit) (TType (UVar -1)))) (P (DCon 0 0) (UN MkUnit) (P (TCon 0 0) (UN Unit) Erased))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 8 0) (UN Unit) (TType (UVar -1))))))
--------------
(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 48))) (TType (UVar 50))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 52))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 8 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 54)))))
--------------
(App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48)))) (App (App (App (App (P (DCon 0 4) (UN MkPair) (Bind (UN A) (Pi (TType (UVar -1))) (Bind (UN B) (Pi (TType (UVar -1))) (Bind (UN a) (Pi (V 1)) (Bind (UN b) (Pi (V 1)) (App (App (P (TCon 0 0) (UN Pair) Erased) (V 3)) (V 2))))))) (TType (UVar 42))) (TType (UVar 44))) (TType (UVar 48))) (TType (UVar 48))))