proposition: Lemma not_Rh_var x u : ~ Var x ->Rh u.
proof: Proof. intro r; inversion r; clear r. destruct H; inversion H. inversion H; subst; clear H. revert H0. destruct (rule_ok H1) as [f [n [ls h]]]; subst; clear H1. rewrite subs_apps. destruct ls; simpl. discr. rewrite apps_app. discr. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(LogicUtil RelUtil VecOrd VecUtil LAlpha)