proposition: Lemma subs1_notin_fv : forall u s, domain (fv u) s [=] empty -> subs1 s u = u.
proof: Proof. induction u; intro s; simpl. intro h. eapply notin_domain. apply h. set_iff. refl. refl. rewrite domain_union, union_empty. intros [h1 h2]. rewrite IHu1, IHu2; auto. intro h. rewrite IHu. refl. rewrite domain_update_id. hyp. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)