proposition: Fact ra_ite_val b p q : ⟦ra_ite⟧ (b##p##q##vec_nil) (ite_rel b p q).
proof: Proof. simpl; unfold s_rec. induction b as [ | b IHb ]; simpl; auto. exists (ite_rel b p q); split; auto. 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)