proposition: Lemma Cont_parametricity : forall A B C (f : B -> C) (g : A -> B) (k : forall r, Cont r A), f (k B g) = k C (f \o g).
proof: Proof. intros. Import YonedaLaws. pose proof (@Yoneda_parametricity Identity _ _ _ _ k f). apply H. Qed.
imports: Hask.Prelude Hask.Control.Monad Hask.Data.Functor.Identity Hask.Data.Functor.Yoneda