[Agda] `postulate' under `with'

[Sergei Meshveliani]

People,
I have a code fragment 

   e : ((L +' p+p') +' <ps>) =al (L +' (p+p' +' <ps>))        -- (I)
   e  with k' ≟ k
   ... | yes _   =  +'assoc₂aux (k , m' + m) L <ps> ps PE.refl
   ... | no k'≉k =  e0
     where
     postulate
       e0 : ((L +' p+p') +' <ps>) =al (L +' (p+p' +' <ps>))   -- (II)


in which I need to elaborate further a proof for  e0:

     e0 = begin.. ...
          end 

But at least, I need to start with some correct expression for (II).
And the type checker rejects the type  (II), even despite that (II)
postulates (I).

What is the simplest way to initially postulate for  e0  something that
fits the goal  e  ?

Thanks,

------
Sergei