proposition: Lemma subs1_single_id y u : subs1 (single y (Var y)) u = u.
proof: Proof. rewrite <- subs1_id. apply subs1_seq. intros x hx. unfold Def.single, Def.update. eq_dec x y. subst. refl. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)