proposition: Lemma R__P_injective n m: R__P n = R__P m -> n = m.
proof: Proof. induction n in m |-*; destruct m; cbn; eauto. 1: destruct (R__P m) as [[] b]; discriminate. 1: destruct (R__P n) as [[] b]; discriminate. destruct (R__P n) as [[|k] p] eqn: H1, (R__P m) as [[|k'] p'] eqn: H2. all: injection 1; intros; subst. all: erewrite IHn; eauto. all: discriminate. Qed.
imports: FinFun Undecidability.HOU(std.decidable)