proposition: Lemma eqset_app_if : forall T (l1 l2 l3 l4 : list T), @eqset T l1 l3 -> @eqset T l2 l4 -> @eqset T (l1 ++ l2) (l3 ++ l4).
proof: Proof. unfold eqset; introv eqs1 eqs2; introv. repeat (rw in_app_iff). rw eqs1; rw eqs2; sp. Qed.
imports: UsefulTypes bin_rels Omega