[Agda] `postulate' under `with'

[flicky frans]

You can postulate False:

   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 =  undefined where
      postulate
         undefined : ∀ {α} {A : Set α} -> A