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