proposition: Fact prim_rec_bool_spec n f : @prim_rec_bool n f = true <-> prim_rec f.
proof: Proof. induction f as [ x | | | n p | n i f g Hf Hg | n f g Hf Hg | n f Hf ]; simpl; try tauto. + rewrite andb_true_iff, fold_right_andb, <- Forall_forall. rewrite Forall_map, Forall_forall, Hf. split; intros (? & H); split; auto. * intros p; apply Hg, H, pos_list_prop. * intros x Hx; apply Hg, H. + rewrite andb_true_iff, Hf, Hg; tauto. + split; try tauto; discriminate. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec