proposition: Lemma E_weaken s ρ p : E (ren_poly_type shift s) (p .: ρ) == E s ρ.
proof: Proof. intros P. eapply R_ext. eapply V_weaken. reflexivity. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms