theorem eqtr4i (a b c: nat): $ a = b $ > $ c = b $ > $ a = c $;
a = b -> c = b -> a = c
a = b
c = b -> a = c
c = b
a = c