proposition: Fact finite_t_fin_upto : finite_t_upto ≅ fin_t_upto (fun _ => True).
proof: Proof. split; intros []; red; eauto; firstorder. Qed.
imports: List Arith Nat Lia Relations Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list fin_base)