384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maedervar a : Type; b < a_v1

01996e191c1a9a2251abf7740124b73bde771472Christian Maederop twice2

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder : forall a : Type; b < a_v1 : Type .

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v-1 ->? b_v-2) -> a_v-1 ->? b_v-2

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder = \ (var f : a ->? b)(var x : a)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder . ((var f : a ->? b)((var f : a ->? b)(var x : a) : b) : b) as b_v2

01996e191c1a9a2251abf7740124b73bde771472Christian Maederop twice3

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder : forall a : Type; b < a_v1 : Type .

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v-1 ->? b_v-2) * a_v-1 ->? b_v-2

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder = ((\ (var f : a ->? b, var x : a)

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder . (var f : a ->? b)((var f : a ->? b)(var x : a) : b) : b) :

d48085f765fca838c1d972d2123601997174583dChristian Maeder (a ->? b) * a ->? b) as

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v1 ->? b_v2) * a_v1 ->? b_v2

01996e191c1a9a2251abf7740124b73bde771472Christian Maederop twice

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder : forall a : Type; b < a_v1 : Type .

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v-1 ->? b_v-2) -> a_v-1 ->? b_v-2

d48085f765fca838c1d972d2123601997174583dChristian Maeder = ((\ (var f : a ->? a)(var x : a)

d48085f765fca838c1d972d2123601997174583dChristian Maeder . (var f : a ->? a)((var f : a ->? a)(var x : a) : a) : a) :

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder (a ->? a) -> a ->? a) as

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v1 ->? b_v2) -> a_v1 ->? b_v2

01996e191c1a9a2251abf7740124b73bde771472Christian Maedervar f : a ->? b; x : a

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder. ((fun __=__[b] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder b * b ->? Unit)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder ((((op twice[a; b]

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder : forall a : Type; b < a_v1 : Type .

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v-1 ->? b_v-2) -> a_v-1 ->? b_v-2) :

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a ->? b) -> a ->? b)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (var f : a ->? b) :

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder a ->? b)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (var x : a) :

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder b,

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (var f : a ->? b)((var f : a ->? b)(var x : a) : b) : b) :

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder Unit

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

d48085f765fca838c1d972d2123601997174583dChristian Maeder? : +Type -> Type

d48085f765fca838c1d972d2123601997174583dChristian MaederLogical : Type := ? 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)%

d48085f765fca838c1d972d2123601997174583dChristian Maeder = ((\ (var f : a ->? a)(var x : a)

d48085f765fca838c1d972d2123601997174583dChristian Maeder . (var f : a ->? a)((var f : a ->? a)(var x : a) : a) : a) :

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder (a ->? a) -> a ->? a) as

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v1 ->? b_v2) -> a_v1 ->? b_v2

01996e191c1a9a2251abf7740124b73bde771472Christian Maedertwice2

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder : forall a : Type; b < a_v1 : Type .

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v-1 ->? b_v-2) -> a_v-1 ->? b_v-2

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder %(op)%

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder = \ (var f : a ->? b)(var x : a)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder . ((var f : a ->? b)((var f : a ->? b)(var x : a) : b) : b) as b_v2

01996e191c1a9a2251abf7740124b73bde771472Christian Maedertwice3

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder : forall a : Type; b < a_v1 : Type .

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v-1 ->? b_v-2) * a_v-1 ->? b_v-2

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder %(op)%

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder = ((\ (var f : a ->? b, var x : a)

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder . (var f : a ->? b)((var f : a ->? b)(var x : a) : b) : b) :

d48085f765fca838c1d972d2123601997174583dChristian Maeder (a ->? b) * a ->? b) as

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v1 ->? b_v2) * a_v1 ->? b_v2

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

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder%% Variables -------------------------------------------------------------

01996e191c1a9a2251abf7740124b73bde771472Christian Maederf : a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maederx : a

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder%% Sentences -------------------------------------------------------------

01996e191c1a9a2251abf7740124b73bde771472Christian Maederforall f : a ->? b; x : a

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder . (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder ((op twice2

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder : forall a : Type; b < a_v1 : Type .

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v-1 ->? b_v-2) -> a_v-1 ->? b_v-2)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (var f : a ->? b)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (var x : a),

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder ((var f : a ->? b)((var f : a ->? b)(var x : a) : b) : b) as

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder b_v2) %(def_twice2)%

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (op twice3

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder : forall a : Type; b < a_v1 : Type .

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v-1 ->? b_v-2) * a_v-1 ->? b_v-2,

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder ((\ (var f : a ->? b, var x : a)

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder . (var f : a ->? b)((var f : a ->? b)(var x : a) : b) : b) :

d48085f765fca838c1d972d2123601997174583dChristian Maeder (a ->? b) * a ->? b) as

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v1 ->? b_v2) * a_v1 ->? b_v2) %(def_twice3)%

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder(fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (op twice

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder : forall a : Type; b < a_v1 : Type .

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v-1 ->? b_v-2) -> a_v-1 ->? b_v-2,

d48085f765fca838c1d972d2123601997174583dChristian Maeder ((\ (var f : a ->? a)(var x : a)

d48085f765fca838c1d972d2123601997174583dChristian Maeder . (var f : a ->? a)((var f : a ->? a)(var x : a) : a) : a) :

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder (a ->? a) -> a ->? a) as

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v1 ->? b_v2) -> a_v1 ->? b_v2) %(def_twice)%

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder((fun __=__[b] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder b * b ->? Unit)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder ((((op twice[a; b]

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder : forall a : Type; b < a_v1 : Type .

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a_v-1 ->? b_v-2) -> a_v-1 ->? b_v-2) :

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (a ->? b) -> a ->? b)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (var f : a ->? b) :

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder a ->? b)

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (var x : a) :

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder b,

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder (var f : a ->? b)((var f : a ->? b)(var x : a) : b) : b) :

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder Unit

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

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

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder*** Hint 9.7, not a kind 'a ->? b'

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder*** Hint 9.20, not a class 'a'