proposition: Lemma single_update_var x u v s : subs (comp (single (var x u s) v) (update x (Var (var x u s)) s)) u = subs (update x v s) u.
proof: Proof. apply single_update. 2: apply var_notin_fvcodom. unfold Def.var; ens. set (xs := fvcodom (remove x (fv u)) s). gen (var_notin_ok (union (fv u) xs)). destruct (mem x xs); set_iff; fo. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)