Different equality types treated as the same in typechecking

[ShreckYe]

This is another issue I encountered while trying to complete the last exercise in Universes, Induction, Specifications - Arend Theorem Prover.

\func \infixl 6 - (x y : Nat) : Nat
  | 0, _ => 0
  | suc x, 0 => suc x
  | suc x, suc y => x - y

\func ss/2 (n : Nat) : Nat
  | 0 => 1
  | 1 => 1
  | suc (suc n) => suc (ss/2 n)

\func ss-ss/2 (n : Nat) : Nat =>
  suc (suc n) - ss/2 n

\func s[ssn/2]-ssssn/2] (n : Nat) : suc (ss/2 n) = ss/2 (suc (suc n))
  | 0 => idp
  | 1 => idp
  | suc (suc n) => pmap suc (s[ssn/2]-ssssn/2] n)

\func s[ssn-ssn/2]=ssssn-ssssn/2 (n : Nat) : suc (ss-ss/2 n) = ss-ss/2 (suc (suc n))
  | 0 => idp
  | 1 => idp
  | suc (suc n) => s[ssn-ssn/2]=ssssn-ssssn/2 n -- Shouldn't it be `pmap suc (s[ssn-ssn/2]=ssssn-ssssn/2 n)` here?

\func test-0 : suc (ss-ss/2 0) = 2 => idp
\func test-0' : ss-ss/2 (suc (suc 0)) = 2 => idp
\func test-0'' : (suc (ss-ss/2 0) = ss-ss/2 (suc (suc 0))) = (2 = 2) => idp

\func test-1 : suc (ss-ss/2 1) = 3 => idp
\func test-1' : ss-ss/2 (suc (suc 1)) = 3 => idp

\func test-2 : suc (ss-ss/2 2) = 3 => idp
\func test-2' : ss-ss/2 (suc (suc 2)) = 3 => idp
\func test-2'' : (suc (ss-ss/2 2) = ss-ss/2 (suc (suc 2))) = (3 = 3) => idp

\func test-3 : suc (ss-ss/2 3) = 4 => idp
\func test-3' : ss-ss/2 (suc (suc 3)) = 4 => idp

In the suc (suc n) case of s[ssn-ssn/2]=ssssn-ssssn/2, the code simply recursively calls itself and typechecks, which implies that s[ssn-ssn/2]=ssssn-ssssn/2 2 should have the same type with s[ssn-ssn/2]=ssssn-ssssn/2 0. However seeing from the tests below, s[ssn-ssn/2]=ssssn-ssssn/2 0 should have the type 2 = 2 and s[ssn-ssn/2]=ssssn-ssssn/2 2 should have the type 3 = 3 which are clearly different types of =.

[valis]

It's fixed. Btw, pmap suc (s[ssn-ssn/2]=ssssn-ssssn/2 n) won't work there.