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