ad53c2449238379699243be05926645262e9581eChristian Maedervars a : Type; b < a

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskiop twice2 (f : a ->? b) (x : a) :? b = f(f(x))

7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maederop twice3 : (a ->? b) * a ->? b = \ (f : a ->? b, x : a) . f(f(x))

e899b993b4f642217274fda6f462fe1318ae3626Christian Maeder

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maederop twice : (a ->? b) -> a ->? b = \ f (x : a) . f(f(x))

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedervar f : a ->? b; x : a

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski

679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski. twice f x = f(f(x))

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder