proposition: Lemma eval_weaken s ρ d : eval (d .: ρ) (ren_poly_type shift s) == eval ρ s.
proof: Proof. now rewrite eval_ren. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms