proposition: Lemma lam_beta_aeq_l x u v : Lam x u =>b v -> exists y w, v = Lam y w /\ u =>b rename y x w.
proof: Proof. intro r; inversion r; clear r; subst. inv_aeq H; clear H; subst. permut_rename i0. inversion H1; clear H1; subst. inversion H. inv_aeq H0; clear H0; subst. ex x1 u1. split. refl. rewrite i3, i, rename2. 2: hyp. apply subs_beta_aeq. refl. apply clos_aeq_intro_refl. hyp. Qed.
imports: Coq(Wf_nat Basics Morphisms) CoLoR(RelUtil LogicUtil VecUtil VecOrd SN NatUtil)