Added a canonical agreement, added trans_agreement, declared a simpl
Theorem and proved it.