proposition: Fact E_unique n m x y1 y2: E n x = Some y1 -> E m x = Some y2 -> y1 = y2.
proof: Proof. induction n in x, m |-*; destruct m; try discriminate. cbn; destruct delta; eauto; now intros [= ->] [= ->]. Qed.
imports: Morphisms FinFun ConstructiveEpsilon Undecidability.HOU(std.tactics std.decidable std.misc std.ars.basic std.ars.confluence)