proposition: Lemma subs_lam s x u : subs s (Lam x u) = subs (update x (Var x) s) (Lam x u).
proof: Proof. set (s' := update x (Var x) s). simpl. set (p := remove x (fv u)). assert (h : fvcodom p s [=] fvcodom p s'). intro y. rewrite !In_fvcodom. split; intros [z [h1 [h2 h3]]]. exists z. unfold s'. unfold Def.update. eq_dec z x. subst z. absurd (In x p). unfold p. set_iff. tauto. hyp. intuition. exists z. revert h2 h3. unfold s'. unfold Def.update. eq_dec z x. subst z. tauto. tauto. assert (e : var x u s = var x u s'). unfold Def.var; ens. fold p. rewrite h. destruct (mem x (fvcodom p s')). rewrite h. refl. refl. rewrite e. set (x' := var x u s'). unfold s'. rewrite update2_eq. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)