proposition: Lemma R_ren ξ1 ξ2 p P : R p P -> R p (ren_term ξ1 ξ2 P).
proof: Proof. induction 1 as [P H H0 H1]. econstructor. - intros HnP ξ'1 ξ'2. asimpl. eapply H. now destruct P. - intros Q. erewrite rinst_inst_term; try reflexivity. intros (P' & H2 & <-) % step_subst_inv. erewrite <- rinst_inst_term; try reflexivity. eauto. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms