proposition: Lemma subs1_update_single x y y' : forall u s, ~In y (bv u) -> subs1 (update y (Var y') s) (subs1 (single x (Var y)) u) = subs1 (update x (Var y') (update y (Var y') s)) u.
proof: Proof. induction u; intro s; simpl; set_iff; intro hy. rename x0 into z. unfold Def.single. unfold Def.update at -1. eq_dec z x; simpl. rewrite update_eq. refl. unfold Def.update. eq_dec z y; refl. refl. rewrite IHu1, IHu2; auto. rename x0 into z. f_equal. eq_dec z x. subst z. rewrite subs1_update2_eq, subs1_update_single_eq, subs1_single_id. refl. rewrite subs1_update2_neq_com. 2: tauto. rewrite subs1_update_id_single. 2: tauto. rewrite IHu; auto. apply subs1_seq. intros a ha. unfold Def.update. eq_dec a x; eq_dec a y; eq_dec a z; try subst a; try subst x; try subst y; tauto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)