384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maedervar a : Type; b < a_v1

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederop twice : (a ->? b) -> a ->? b

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder %% = \ (f : a ->? b) (x : a) . f(f(x))

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder%% Type Constructors -----------------------------------------------------

c81507d35d11b2eedf7425a3bb52bceec3224532Christian MaederLogical : Type := Unit ->? Unit

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian MaederPred : -Type -> Type := \ a : -Type . a_v-1 ->? Unit

c81507d35d11b2eedf7425a3bb52bceec3224532Christian MaederUnit : Type

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__*__ : +Type -> +Type -> Type

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maeder__*__*__ : +Type -> +Type -> +Type -> Type

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maeder__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maeder__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__-->?__ : -Type -> +Type -> Type < __->?__

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__->__ : -Type -> +Type -> Type < __->?__

bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2Christian Maeder__->?__ : -Type -> +Type -> Type

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maeder%% Type Variables --------------------------------------------------------

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maedera : Type %(var_1)%

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maederb < a_v1 : Type %(var_2)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder%% Assumptions -----------------------------------------------------------

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__if__ : ? Unit * ? Unit ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder__when__else__

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder : forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederbottom : forall a : Type . a_v-1 %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederdef__ : forall a : Type . a_v-1 ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederfalse : Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maedernot__ : ? Unit ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maedertrue : Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maedertwice

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maeder : forall a : Type; b < a_v1 : Type .

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maeder (a_v-1 ->? b_v-2) -> a_v-1 ->? b_v-2

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder %(op)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder�__ : ? Unit ->? Unit %(fun)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder%% Diagnostics -----------------------------------------------------------

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder*** Hint 1.6, is type variable 'a'