proposition: Lemma R_aeq_apps_neutral : forall n (us : Tes n) u v, neutral u -> apps u us =>R v -> (exists u', v ~~ apps u' us /\ u =>R u') \/ (exists us', v ~~ apps u us' /\ Vrel1 R_aeq us us').
proof: Proof. induction us as [|a n us IHus]; simpl; intros u v nu r. left. exists v. split. refl. hyp. destruct (IHus _ _ (neutral_app a nu) r). destruct H as [w [h1 h2]]. destruct (R_aeq_app_neutral nu h2). destruct H as [u' [i1 i2]]. left. exists u'. split. rewrite h1, i1. refl. hyp. destruct H as [a' [i1 i2]]. right. exists (Vcons a' us). split. rewrite h1, i1. refl. apply left_sym. hyp. destruct H as [us' [h1 h2]]. right. exists (Vcons a us'). split. rewrite h1. refl. apply right_sym. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)