feat(Computability): r.e. sets are closed under inter/union/projection/composition

[iehality]

Prove that r.e. sets are closed under intersections, unions, projection and composition.

---

[github-actions]

PR summary 12251580db

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ comp_computable
+ const
+ inter
+ re_iff
+ union
+++ projection

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[YaelDillies]

Can you use aesop to golf anything?

[YaelDillies]

Can you squeeze that simp?

[YaelDillies]

Suggested change

	by_cases h : p <;> simp [h]
	· simpa using Partrec.some.dom_re
	· simpa using (Partrec.none (α := α) (σ := α)).dom_re
	by_cases h : p
	· simpa [h] using Partrec.some.dom_re
	· simpa [h] using (Partrec.none (α := α) (σ := α)).dom_re