proposition: Fact nat2bt_inj n m : nat2bt n ≈ nat2bt m -> n = m.
proof: Proof. revert m; induction n as [ | n IHn ]; intros [ | m ]; simpl; auto. + intros H; symmetry in H; apply bte_discr in H; tauto. + intros H; apply bte_discr in H; tauto. + intros H; rewrite bte_ext in H. f_equal; apply IHn; clear IHn. generalize (proj1 (H (nat2bt n))) (proj2 (H (nat2bt m))); btm simpl. intros [H0 | H0] [H1 | H1]; auto. apply btm_depth in H0. apply btm_depth in H1. lia. Qed.
imports: List Arith Lia Max Wellfounded Setoid Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_decidable finite seteq) Undecidability.Shared.Libs.DLW.Vec(pos) Undecidability.Shared.Libs.DLW.Wf(wf_finite wf_chains) Undecidability.FOL.TRAKHTENBROT(notations fol_ops)