[Agda] congruence, Preserves_2

[Serge D. Mechveliani]

On Sat, Sep 08, 2012 at 10:38:26PM +0400, Serge D. Mechveliani wrote:
[..]
>   p : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
>   p m n p =  ?
[..]

For any occasion, change it to  

  proo : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
  proo m n p =  ?

------
Sergei