p,q,r,s:
. p =q q 
r =q s p *q r =q q *q sx,y:
. x=
y 
x = yi1,i2,j1,j2:. i1 = j1 i2 = j2 i1
i2 = j1j2| Rank | Theorem | Name |
| 2 | p,q,r,s:. p =q q r =q s p *q r =q q *q s | [qmul_functionality] |
| cites the following: | ||
| 1 | x,y:. x=y x = y | [assert_of_eq_int_rw] |
| 0 | i1,i2,j1,j2:. i1 = j1 i2 = j2 i1i2 = j1j2 | [mul_functionality_wrt_eq] |