proposition: Lemma RcR_idRen_right {Γ Γ'} (σ : Ren Γ Γ') : RcR σ idRen = σ.
proof: Proof. induction σ; simp RcR; simpl; simp RcR; auto; now rewrite IHσ. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Equations(Equations)