proposition: Theorem rev_exercise1 : forall (l l' : list nat), l = rev l' -> l' = rev l.
proof: Proof. Admitted. Example trans_eq_example : forall (a b c d e f : nat), [a;b] = [c;d] -> [c;d] = [e;f] -> [a;b] = [e;f]. Proof. intros a b c d e f eq1 eq2. rewrite -> eq1. rewrite -> eq2. reflexivity. Qed.