proposition: Lemma subset_compat_2 : forall s1 s2 s2', eq_set s2 s2' -> subset s1 s2 -> subset s1 s2'.
proof: Proof. intros s1 s2 s2' s2_eq_s2' H e e_in_s1; generalize (s2_eq_s2' e) (H e e_in_s1); intuition. Qed.
imports: List more_list list_permut Arith