proposition: Lemma RenExp_RcR {τ Γ Γ' Γ''} (σ : Ren Γ' Γ'') (δ : Ren Γ Γ') (e : Exp Γ'' τ) : RenExp (RcR σ δ) e = RenExp δ (RenExp σ e).
proof: Proof. generalize dependent Γ'. generalize dependent Γ. induction e; simpl; intros; auto; rewrite ?IHe, ?IHe1, ?IHe2, ?IHe3; auto. - now rewrite RenVar_RcR. - now rewrite <- IHe; simp RcR. Qed.
imports: Coq.Lists.List Category.Lib Category.Instance.Lambda.Exp Category.Instance.Lambda.Value Equations(Equations)