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. hyp. inversion H. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)