Congruence Rejection From Simplification Premise Containing Negative Arguments

[m4mbo]

After some experimenting with the limits of the congruence rule, I found out that carcara is currently rejecting the application of said rule on operations that contain negative arguments. Ex:

Input:

(step t18 (cl (= (+ 2 (- 1)) 1)) :rule sum_simplify)
(step t19 (cl (= (= 2 (+ (+ 0 (+ 2 (- 1))) 1)) (= 2 (+ (+ 0 1) 1)))) :rule cong :premises (t18))

Output (from carcara):

[ERROR] checking failed on step 't19' with rule 'cong': premise '(= (+ 2 (- 1)) 1)' doesn't justify conclusion arguments '(+ (+ 0 (! (+ 2 (- 1)) :named @p_0)) 1)' and '(+ (+ 0 1) 1)' invalid

I understand that the simplification could be expressed as:

(step t18 (cl (= (- 2 1) 1)) :rule minus_simplify)

But, if that is the requirement, I believe you should be getting an error on the simplification step rather than the congruence itself. I am opening this discussion to hear what are your opinions on the issue. Should carcara be able to accept this cong application?