proposition: Lemma subs1_update_id_single y v x u : x<>y \/ v=Var x -> subs1 (update x (Var x) (single y v)) u = subs1 (single y v) u.
proof: Proof. intro h. apply subs1_seq. intros b hb. unfold Def.single, Def.update. eq_dec b x; eq_dec b y. subst. destruct h. tauto. subst. refl. subst. refl. refl. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)