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