proposition: Lemma lam_eta_aeq_l x u v : Lam x u =>e v -> (exists v', u = App v' (Var x) /\ ~In x (fv v') /\ v' ~~ v) \/ (exists y w, v = Lam y w /\ (x=y \/ ~In y (fv u)) /\ u =>e rename y x w).
proof: Proof. rename x into x0. rename u into u0. rename v into v0. intro e; inversion e; clear e; subst; rename v' into v1. inv_aeq H; clear H; subst. permut_rename i0; clear i1. rename x into x1. rename u into u1. inversion H1; clear H1; subst. left. inversion H; clear H; subst. rewrite rename_app, rename_var, eqb_refl, rename_notin_fv in i. 2: hyp. inv_aeq i; clear i; subst; rename u into v2. ex v2. split. refl. split. 2: trans v1; hyp. revert i2. simpl. set_iff. rewrite i1. split_all. subst. contr. right. inv_aeq H0; clear H0; subst. rename x into x2; rename u into u2'; rename u' into u1'. ex x2 u2'. split. refl. split. 2:{ rewrite i, i1, rename2. apply subs_eta_aeq. refl. apply clos_aeq_intro_refl. hyp. hyp. } permut_rename i1; clear i3. split_all; subst; try rewrite rename_id in *. auto. rewrite i, fv_rename. apply notin_replace. rewrite i, H4, i0, fv_rename. apply notin_replace. rewrite i, fv_rename, H4, i0, fv_rename, replace2. apply notin_replace. auto. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil RelUtil VecOrd VecUtil)