proposition: Lemma iso_impl : @subrelation Prop isomorphic Basics.impl.
proof: Proof. unfold subrelation, predicate_implication, pointwise_lifting. intros A B. unfold Basics.impl. intros H x. do 2 destruct H. exact (x0 x). Qed.
imports: Hask.Ltac Hask.Prelude Hask.Control.Applicative Hask.Control.Monad Hask.Control.Monad.Cont Hask.Control.Monad.State Hask.Data.Functor.Contravariant Hask.Data.Functor.Identity Hask.Data.Functor.Kan Hask.Data.Functor.Yoneda Hask.Control.Lens Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Init.Datatypes Coq.Relations.Relation_Definitions FunctionalExtensionality