Proving the Functor laws for free monads; am I doing it right?

I'm having a bit of a hard time understanding how to prove the Functor and Monad laws for free monads. First off, let me put up the definitions I'm using:

data Free f a = Pure a | Free (f (Free f a))

instance Functor f => Functor (Free f) where
    fmap f (Pure a) = Pure (f a)
    fmap f (Free fa) = Free (fmap (fmap f) fa)

instance Functor f => Monad (Free f) where
    return = Pure
    Pure a >>= f = f a
    Free fa >>= f = Free (fmap (>>=f) fa)

{-

Functor laws:
(1) fmap id x == x
(2) fmap f (fmap g x) = fmap (f . g) x

Monad laws:
(1) return a >>= f   ==  f a
(2) m >>= return     ==  m
(3) (m >>= f) >>= g  ==  m >>= (\x -> f x >>= g)

-}

If I understand things correctly, the equational proofs require appeal to a coinductive hypothesis, and it goes more or less like this example:

Proof: fmap id == id

Case 1: x := Pure a
fmap id (Pure a)
  == Pure (id a)   -- Functor instance for Free
  == Pure a        -- id a == a

Case 2: x := Free fa
fmap id (Free fa)
  == Free (fmap (fmap id) fa)  -- Functor instance for Free f
  == Free (fmap id fa)         -- By coinductive hypothesis; is this step right?
  == Free fa                   -- Functor f => Functor (Free f), + functor law 

I've highlighted the step where I'm not sure if I'm doing things right.

If that proof is right, then the proof for the Free constructor case of the second law is as follows:

fmap f (fmap g (Free fa))
  == fmap f (Free (fmap (fmap g) fa))
  == Free (fmap (fmap f) (fmap (fmap g) fa))
  == Free (fmap (fmap f . fmap g) fa)
  == Free (fmap (fmap (f . g)) fa)           -- By coinductive hypothesis
  == fmap (f . g) (Free fa)