米田の補題

y : (X -> ((A -> X) -> F X)) -> F A
y T := T A id