proposition: Lemma R_step p P Q : step P Q -> R p P -> R p Q.
proof: Proof. intros ? []. eauto. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms