proposition: Fact ra_ite_0 p q : ⟦ra_ite⟧ (0##p##q##vec_nil) p.
proof: Proof. apply ra_ite_val. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list gcd crt sums finite pos vec) Undecidability.MuRec.Util(recalg recomp prim_min)