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