proposition: Theorem trans_law_1_x : forall (T : (Type -> Type) -> Type -> Type) {M : Type -> Type} `{m : MonadLaws M} `{tm : MonadLaws (T M)} `{MonadTransLaws T} {A : Type} {x : A}, lift (pure[M] x) = (@pure (T M) _ A) x.
proof: Proof. intros. destruct H2. specialize (trans_law_3 M _). rewrite <- trans_law_3. reflexivity. assumption. assumption. Qed.
imports: Hask.Prelude Hask.Control.Monad