a:
. (-a) ~ aa,b:. a | b 
-a | ba:. a | aa,b:. a | b a | -b| Rank | Theorem | Name |
| 2 | a:. (-a) ~ a | [neg_assoced] |
| cites the following: | ||
| 0 | a,b:. a | b -a | b | [divides_invar_1] |
| 0 | a:. a | a | [divides_reflexivity] |
| 1 | a,b:. a | b a | -b | [divides_invar_2] |