proposition: Lemma RcR_assoc {Γ Γ' Γ'' Γ'''} (σ : Ren Γ'' Γ''') (δ : Ren Γ' Γ'') (ν : Ren Γ Γ') : RcR (RcR σ δ) ν = RcR σ (RcR δ ν).
proof: Proof. generalize dependent Γ'''. generalize dependent Γ''. induction ν; simp RcR; simpl; intros; auto. - simp RcR. now rewrite IHν. - dependent elimination δ; simp RcR; simpl. + now rewrite IHν. + dependent elimination σ; simp RcR; simpl; now rewrite IHν. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Equations(Equations)