proposition: Lemma Rh_eh x u w : Lam x u ->Rh w -> Lam x u ->eh w.
proof: Proof. intro r; inversion r; clear r. destruct H. inversion H. hyp. 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)