proposition: Lemma step_ext_2 P Q1 Q2 : step P Q1 -> Q1 = Q2 -> step P Q2.
proof: Proof. now intros ? ->. Qed.
imports: Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util.typing_facts Undecidability.SystemF.Util.term_facts Coq.Relations.Relation_Operators