c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maedervars a : Type; b < a

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederop twice2 (f : a ->? b) (x : a) :? b = f(f(x))

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maederop 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))

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

. twice f x = f(f(x))