[Agda] "with .. postulate"

[Serge D. Mechveliani]

On Wed, Mar 06, 2013 at 08:11:56PM +0100, Andreas Abel wrote:
> Your definition of 'go' almost works, you only have to abstract over
> (invMb a).  Calling this abstraction 'r', I get the following code
> which type-checks.
> 
>     go : (r : Maybe (Dec (Inverse {M = Mg} e a))) ->
>          justYes? r \equiv true -> justYes? (invMb-sub a') \equiv true
> 
>     go nothing                    ()
>     go (just (no _))              ()
>     go (just (yes (i , iProofs))) _ =  afterInv
>        where
>        postulate afterInv : justYes? (invMb-sub a') \equiv true
> 

(I have changed a couple of math symbols)

> Hope this helps!

Indeed, it helps. Thank you.
I see now that my version of `go' did not really present a proof.

And the subject is new for me.
Before yesterday I thought: 
  if I have a simple intuitive mathematical and constructive proof for a 
  statement, then it needs no real invention to convert it to a proof for
  Agda.

And now I start to doubt in this. Because one also needs to find a 
signature  sig  for helper functions like the above `go'
(consider more complex examples). It needs to be found among many 
possible ones, the argument expressions must belong to  sig,  and  sig
must be special enough to allow a proof.
1) I need to gain experience in this.
2) What people think of this:
   provided that the implemnentation part is given, to what extent 
   finding a sufficient signature can be automated in general?
   
(for note that my `go' and your `go' have the same implementation code).

Thanks,

------
Sergei