vars a : Type; b < a

op twice2(f : a ->? b) (x : a) :? b = f (f x);

op twice3 : (a ->? b) * a ->? b =

\ (f : a ->? b, x : a) . f (f x);

op twice : (a ->? b) -> a ->? b = \ (f)(x : a) . f (f x);

vars f : a ->? b; x : a

. twice f x = f (f x);

%% Type Variables --------------------------------------------------------

a : Type %(var_1)%

b < a : Type %(var_2)%

%% Assumptions -----------------------------------------------------------

twice

: forall a : Type; b < a : Type . (a ->? b) -> a ->? b

%(op)% =

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

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

as (a ->? b) -> a ->? b

twice2

: forall a : Type; b < a : Type . (a ->? b) -> a ->? b

%(op)% =

\ ((var f : a ->? b))((var x : a))

. (var f : a ->? b) ((var f : a ->? b) (var x : a)) as b

twice3

: forall a : Type; b < a : Type . (a ->? b) * a ->? b

%(op)% =

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

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

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

%% Variables -------------------------------------------------------------

f : a ->? b

x : a

%% Sentences -------------------------------------------------------------

forall f : a ->? b; x : a . twice2 f x = (f (f x) as b)

%(def_twice2)%

twice3

= ((\ (f : a ->? b, x : a) . f (f x)) as (a ->? b) * a ->? b)

%(def_twice3)%

twice = ((\ (f)(x : a) . f (f x)) as (a ->? b) -> a ->? b)

%(def_twice)%

twice f x = f (f x)

%% Diagnostics -----------------------------------------------------------

### Hint 1.6, is type variable 'a'

### Hint 9.7, not a kind 'a ->? b'

### Hint 9.20, not a class 'a'