[Agda] Proving m + (1 + n) == 1 + (m + n)

[Jan Stolarek]

Hi *,

I'm trying to figure out how to prove things like m + (1 + n) == 1 + (m + n) so that I can write 
reverse-append function for vectors. I found materials for Computer Aided Formal Reasoning 
(http://www.cs.nott.ac.uk/~txa/g53cfr/) to be quite accessible, but there are some things I don't 
understand. Lecture 9 gives a proof of correctness for reverse-append:

_++'_ : {X : Set} {n m : ℕ} → Vec X n → Vec X m → Vec X (n + m)
_++'_ {X} {zero } {m} []       ys = ys
_++'_ {X} {suc n} {m} (x :: xs) ys =
  subst (Vec X) (sym (+suc n  m)) (xs ++' (x :: ys))

where

+suc : (m n : ℕ) → suc (m + n) ≡ m + (suc n)
+suc zero n = refl
+suc (suc m) n = cong suc (+suc m n)

and cong, subst, refl and sym are imported from Relation.Binary.PropositionalEquality, Nat is from 
Data.Nat and Vec is from Data.Vec. However, if remove import of PropositionalEquality and use 
definitions of cong, subst, refl and sym that were given earlier in the course (lecture 7):

Prp : Set1
Prp = Set

data _==_ {A : Set} : A → A → Prp where
    refl : {a : A} → a == a

sym : {A : Set} → {a b : A} → a == b → b == a
sym refl = refl

cong : {A B : Set} (f : A → B) → forall {x y} → x == y → f x == f y
cong f refl = refl

subst : {A : Set}{P : A → Prp} → {a b : A} → a == b → P a → P b
subst refl p = p

I get error when typechecking second case of _++'_. Typechecker higlights Vec X (first argument to 
subst) and produces an error:

  ℕ → Set !=< _a_55 n x xs ys ≡ _b_56 n x xs ys of type Set₁
  when checking that the expression Vec X has type
  _a_55 n x xs ys ≡ _b_56 n x xs ys

I can't figure out goes wrong here. I looked at the definitions of refl, sym and other functions 
in standard library to see how they differ. I see that refl in std lib operates on other levels 
than just Set. As for other functions thier definition in the library is too difficult for me to 
understand. I would appreciate if someone could explain why the typechecker complains and how to 
fix definitions of refl & friends so that it works.

Janek