proposition: Lemma subs1_update_id x s u : s x = Var x -> subs1 (update x (Var x) s) u = subs1 s u.
proof: Proof. intro h. apply subs1_seq. intros z hz. unfold Def.update. eq_dec z x. subst. auto. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)