0N/Avar a : Type; b < a

3909N/Aop twice2(f : a ->? b) (x : a) :? b = f (f x);

0N/Aop twice3 : (a ->? b) * a ->? b =

0N/A \ (f : a ->? b, x : a) . f (f x);

0N/Aop twice : (a ->? b) -> a ->? b = \ (f)(x : a) . f (f x);

0N/Avar f : a ->? b; x : a

2362N/A. twice f x = f (f x);

0N/A%% Type Variables --------------------------------------------------------

2362N/Aa : Type %(var_1)%

0N/Ab < a : Type %(var_2)%

0N/A%% Assumptions -----------------------------------------------------------

0N/Atwice

0N/A: forall a : Type; b < a : Type . (a ->? b) -> a ->? b

0N/A%(op)% =

0N/A(\ ((var f : a ->? a))((var x : a)) .

0N/A (var f : a ->? a) ((var f : a ->? a) (var x : a)))

0N/Aas (a ->? b) -> a ->? b

0N/Atwice2

0N/A: forall a : Type; b < a : Type . (a ->? b) -> a ->? b

0N/A%(op)% =

2362N/A\ ((var f : a ->? b))((var x : a)) .

2362N/A(var f : a ->? b) ((var f : a ->? b) (var x : a)) as b

2362N/Atwice3

0N/A: forall a : Type; b < a : Type . (a ->? b) * a ->? b

0N/A%(op)% =

862N/A(\ ((var f : a ->? b), (var x : a)) .

0N/A (var f : a ->? b) ((var f : a ->? b) (var x : a)))

0N/Aas (a ->? b) * a ->? b

0N/A%% Variables -------------------------------------------------------------

430N/Af : a ->? b

0N/Ax : a

0N/A%% Sentences -------------------------------------------------------------

0N/Aforall f : a ->? b; x : a . twice2 f x = (f (f x) as b)

0N/A %(def_twice2)%

0N/Atwice3 =

0N/A((\ (f : a ->? b, x : a) . f (f x)) as (a ->? b) * a ->? b)

0N/A %(def_twice3)%

0N/Atwice = ((\ (f)(x : a) . f (f x)) as (a ->? b) -> a ->? b)

0N/A %(def_twice)%

0N/Atwice f x = f (f x)

0N/A%% Diagnostics -----------------------------------------------------------

0N/A### Hint 1.6, is type variable 'a'

0N/A### Hint 9.7, not a kind 'a ->? b'

0N/A### Hint 9.20, not a class 'a'

0N/A