proposition: Lemma RenSem_idRen {Γ} (se : SemEnv Γ) : RenSem idRen se = se.
proof: Proof. induction Γ; destruct se; simpl; simp RenSem; intros; auto. now rewrite IHΓ. 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)