proposition: Lemma not_Rh_app_neutral u v w : neutral u -> ~ App u v ->Rh w.
proof: Proof. intros h r. inversion r; clear r; inversion H; clear H; subst. auto. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)