proposition: Lemma R_app_neutral u v w : neutral u -> App u v ->R w -> (exists u', w = App u' v /\ u ->R u') \/ (exists v', w = App u v' /\ v ->R v').
proof: Proof. intros n r; inversion r; subst. exfalso. eapply not_Rh_app_neutral. apply n. apply H. left. exists u'. auto. right. exists v'. auto. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)