proposition: Lemma subs1_id : forall u, subs1 id u = u.
proof: Proof. induction u; simpl; auto. rewrite IHu1, IHu2. refl. f_equal. rewrite subs1_update_id. hyp. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)