proposition: Lemma aeq_alpha' : forall x u y, x = y \/ ~In y (fv u) -> Lam x u ~~ Lam y (rename x y u).
proof: Proof. intros x u y [h|h]. subst. rewrite rename_id. refl. apply aeq_alpha. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)