proposition: Lemma app_beta_aeq_l u v w : App u v =>b w -> (exists u', w ~~ App u' v /\ u =>b u') \/ (exists v', w ~~ App u v' /\ v =>b v') \/ (exists x, exists a, u = Lam x a /\ w ~~ subs (single x v) a).
proof: Proof. intro r; inversion r; subst. destruct (app_aeq_l H) as [u'1 [v'1 [e [uu'1 vv'1]]]]; subst. inversion H1; subst. inversion H2; subst. right. right. destruct (lam_aeq_l uu'1) as [y [u0' [i1 [i2 i3]]]]; subst. exists y. exists u0'. split. refl. rewrite H0, i2. unfold Def.rename. rewrite subs_comp. apply subs_saeq. intros z hz. unfold Def.comp, Def.single. unfold Def.update at -2. eq_dec z x; simpl. rewrite update_eq. hyp. unfold Def.update. eq_dec z y. destruct i3; subst; tauto. refl. left. destruct (app_aeq_r H0) as [c [d [i1 [i2 i3]]]]. subst. exists u'. split. rewrite <- vv'1. hyp. rewrite <- uu'1. apply incl_clos_aeq. hyp. right. left. destruct (app_aeq_r H0) as [c [d [i1 [i2 i3]]]]. subst. exists v'0. split. rewrite <- uu'1. hyp. rewrite <- vv'1. apply incl_clos_aeq. hyp. Qed.
imports: Coq(Wf_nat Basics Morphisms) CoLoR(RelUtil LogicUtil VecUtil VecOrd SN NatUtil)