proposition: Lemma C_scons s Γ ρ σ P : E s ρ P -> C Γ ρ σ -> C (s .: Γ) ρ (P .: σ).
proof: Proof. intros HE HC. hnf. intros []. eassumption. eapply HC. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms