proposition: Lemma app_eta_aeq_l u v w : App u v =>e w -> exists u' v', w = App u' v' /\ ((u =>e u' /\ v ~~ v') \/ (u ~~ u' /\ v =>e v')).
proof: Proof. intro e; inversion e; clear e; subst. inv_aeq H; clear H; subst. inversion H1; clear H1; subst. inversion H. inv_aeq H0; clear H0; subst. ex u2 u3. split. refl. left. split. 2: trans u1; hyp. eapply clos_aeq_intro. 3: apply H4. hyp. hyp. inv_aeq H0; clear H0; subst. ex u2 u3. split. refl. right. split. trans u0; hyp. eapply clos_aeq_intro. 3: apply H4. hyp. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil VecOrd VecUtil)