proposition: Lemma R_aeq_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. inv_aeq H; clear H; subst. rewrite <- i0 in n. destruct (R_app_neutral n H1) as [h|h]; destruct h as [t [a s]]; subst. left. exists t. rewrite <- i1, <- i0. intuition. apply incl_clos_aeq. hyp. right. exists t. rewrite <- i1, <- i0. intuition. apply incl_clos_aeq. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)