proposition: Lemma eq_set_trans : forall s1 s2 s3, eq_set s1 s2 -> eq_set s2 s3 -> eq_set s1 s3.
proof: Proof. intros s1 s2 s3 s1_eq_s2 s2_eq_s3 e; generalize (s1_eq_s2 e) (s2_eq_s3 e); intuition. Qed.
imports: List more_list list_permut Arith