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);

vars

a : Type %(var_1)%;

b < a : Type %(var_2)%

op 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]%

op 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]%

op 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]%

vars

f : a ->? b;

x : a

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 : a ->? a)(x : a) . f (f x)) as (a ->? b) -> a ->? b)

%(def_twice)%

forall a : Type; b < a : Type; f : a ->? b; x : a

. twice f x = f (f x)

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

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

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