proposition: Lemma subs_rel_update (R : rel Te) xs x u u' s s' : R u u' -> subs_rel R (remove x xs) s s' -> subs_rel R xs (update x u s) (update x u' s').
proof: Proof. intros uu' ss' y hy. unfold Def.update. eq_dec y x. hyp. apply ss'. set_iff. auto. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)