proposition: Lemma lam_R_aeq_l x u v : Lam x u =>R v -> (exists v', u = App v' (Var x) /\ ~In x (fv v') /\ v' ~~ v) \/ (exists y w, v = Lam y w /\ u =>R rename y x w).
proof: Proof. intro r; inversion r; clear r; subst. inv_aeq H; clear H; subst. permut_rename i0; clear i1. inversion H1; clear H1; subst. left. apply Rh_eh in H; inversion H; clear H; subst. rewrite rename_app in i. inv_aeq i; clear i; subst. ex u0. split. rewrite rename_var, eqb_refl in i3. inv_aeq i3. subst. refl. rewrite rename_notin_fv in i1. 2: hyp. rewrite i1. split. 2: hyp. revert i2. simpl. set_iff. split_all. subst. contr. right. inv_aeq H0; clear H0; subst. ex x1 u1. split. refl. rewrite i, i1, rename2. 2: hyp. apply subs_R_aeq. refl. apply clos_aeq_intro_refl. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(RelUtil VecUtil VecOrd LogicUtil SN SetUtil)