proposition: Lemma C_rename Γ ρ σ ξ1 ξ2 : C Γ ρ σ -> C Γ ρ (σ >> ren_term ξ1 ξ2).
proof: Proof. intros H ?. eapply R_ren, H. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms