proposition: Lemma Rh_bh x u v w : App (Lam x u) v ->Rh w -> App (Lam x u) v ->bh w.
proof: Proof. intro r; inversion r; clear r. destruct H. hyp. inversion H. exfalso. inversion H; subst; clear H. revert H0. destruct (rule_ok H1) as [f [n [ls h]]]; subst; clear H1. rewrite subs_apps. simpl. destruct ls; simpl. discr. destruct ls; simpl. discr. rewrite 2!apps_app. discr. Qed.
imports: Coq(Morphisms Basics Lia) CoLoR(LogicUtil RelUtil VecOrd VecUtil LAlpha)