Ну я в итоге несколько часов назад решил отделаться

, тем более что в итоге получилась ошибка в формулировке исчисления, которую я не знаю как исправить, так что ничего больше писать пока не надо. А вообще я почти три раза в исходном посте изобразил, что это должно быть — распилим мысленно

пополам и получим нечто вроде

первым куском, который и интересует (потому что второй-то везде есть).
Предполагалось использовать их в термах типов навроде такого:

, но я честно не понимаю, кому и чем такой пример может что-то пояснить. Главное чтобы два куска воспринимались как части одной распиленной стрелки, потому что они предполагались функционировать как половины функции, одна указывать принятие аргумента и другая выдачу результата.