proposition: Lemma var_subs_rel R : Proper (R ==> Equal) fv -> VarInvL R -> VarInvR R -> forall x u, Proper (subs_rel R (remove x (fv u)) ==> Logic.eq) (var x u).
proof: Proof. intros fv_R R_var_l R_var_r x u s s' ss'. unfold Def.var; ens. rewrite !(fvcodom_subs_rel_Equal fv_R R_var_l R_var_r ss'). refl. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)