a,b,c:
. c
(a
b) = (cb)aa,b:. (a ~ b) 
a = ba,b:. (a
b) ~ (ba)a,b:. (a
b) ~ (ab)BC) ~ (ABC)| Rank | Theorem | Name |
| 11 | a,b,c:. c(ab) = (cb)a | [exp_exp_reduce1] |
| cites the following: | ||
| 4 | a,b:. (a ~ b) a = b | [fin_card_vs_nat_eq] |
| 10 | a,b:. (ab) ~ (ba) | [card_fun_vs_nsub_exp] |
| 8 | a,b:. (ab) ~ (ab) | [nsub_mul_rw] |
| 0 | BC) ~ (ABC) | [card_curry_simple] |