proposition: Lemma R_var p n : R p (var n).
proof: Proof. econstructor. intros [=]. intros Q H. inversion H. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(typing_facts term_facts step) Setoid Morphisms