proposition: Lemma subs_id : forall u, subs id u = u.
proof: Proof. induction u; simpl. refl. refl. rewrite IHu1, IHu2. refl. unfold Def.var; ens. rewrite fvcodom_id, empty_b. f_equal. rewrite <- IHu at 2. apply subs_seq. intros y hy. unfold Def.update. eq_dec y x. rewrite e. refl. refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)