k:
, x,y,z:k.
Thm*
y = z 
x = y (x, y) = compose_list([(x, z); (y, z); (x, z)])i,j:
. i = j (i=
j) = truei,j:. i 
j (i=j) = false| Theorem | Name |
| k:, x,y,z:k.
Thm* y = z x = y (x, y) = compose_list([(x, z); (y, z); (x, z)]) | [flip_lemma] |
| cites the following: | |
| i,j:. i = j (i=j) = true | [eq_int_eq_true] |
| i,j:. i j (i=j) = false | [eq_int_eq_false] |