proposition: Lemma step_fun s t1 t2 : step s t1 -> step s t2 -> t1 = t2.
proof: Proof. move=> H. elim: H t2. - by move=> > /stepE []. - case. + by move=> > /stepE. + by move=> > ? IH ? /stepE [] ? /IH ->. + by move=> > /stepE. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts) Undecidability.L.Util.L_facts Relations Lia ssreflect