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