p,q,r,s:
. p =q q 
r =q s p +q r =q q +q sx,y:
. x=
y 
x = ya,b,n:. a = b n
a = nbi1,i2,j1,j2:. i1 = j1 i2 = j2 i1+i2 = j1+j2| Rank | Theorem | Name |
| 2 | p,q,r,s:. p =q q r =q s p +q r =q q +q s | [qadd_functionality] |
| cites the following: | ||
| 1 | x,y:. x=y x = y | [assert_of_eq_int_rw] |
| 0 | a,b,n:. a = b na = nb | [mul_preserves_eq] |
| 0 | i1,i2,j1,j2:. i1 = j1 i2 = j2 i1+i2 = j1+j2 | [add_functionality_wrt_eq] |