proposition: Lemma C_up s Γ ρ σ : C Γ ρ σ -> C (s .: Γ) ρ (up_term_term σ).
proof: Proof. intros H. eapply C_scons. eapply R_var. now eapply C_rename. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms