proposition: Lemma is_ren_single_var : forall x y, is_renaming (single x (Var y)).
proof: Proof. unfold is_renaming, single. intros. case_beq_nat x x0. exists y. refl. exists x0. refl. Qed.
imports: CoLoR(ATrs VecUtil LogicUtil ListUtil NatUtil VecMax EqUtil RelUtil SN ListMax)