proposition: Fact finite_t_sum X Y : finite_t X -> finite_t Y -> finite_t (X+Y)%type.
proof: Proof. intros H1 H2. apply finite_t_fin_t_eq in H1. apply finite_t_fin_t_eq in H2. apply finite_t_fin_t_eq. generalize (fin_t_sum H1 H2). apply fin_t_equiv. intros []; tauto. Qed.
imports: List Arith Lia Eqdep_dec Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec)