proposition: Lemma RenSem_inil (r : Ren nil nil) : RenSem r () = ().
proof: Proof. now dependent destruction r. Qed.
imports: Category.Lib Category.Lib.IList Category.Instance.Lambda.Ty Category.Instance.Lambda.Exp Category.Instance.Lambda.Ren Category.Instance.Lambda.Sub Equations(Equations)