proposition: Lemma subs1_update_single_id y v x u : subs1 (update y v (single x (Var x))) u = subs1 (single y v) u.
proof: Proof. apply subs1_seq. intros z hz. unfold Def.single. unfold Def.update at -2. eq_dec z y. refl. unfold Def.update. eq_dec z x. subst z. refl. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)