Formalizing splitting into cases Let $x$ denote a fixed but arbitrary real, and suppose we're trying to solve an equation like $$(x^2-1)^2 = 1.$$
The 'high school' approach is to just shuffle the functions on one side onto the other side one at a time, by using the law $$f(x) = y \iff x = f^{-1}(y)$$
All well and good, but there's a problem: namely, that not all functions in sight are necessarily bijective. For instance, the self-map of the real line $x \mapsto x^2$ isn't bijective. To deal with this, the usual approach involves 'splitting into cases', like so:

So the "full-worked solution" the teacher is usually looking for is best understood as some kind of a tree.
The question then arises of what those lines actually mean, in a precise, technical sense. One possible semantics is that $$\frac{P}{Q_0,\cdots,Q_{n-1}} \iff \left(P \iff \mathop{\exists!}_{i \in \mathbb{N}_{<n}} Q_i\right)$$ where $P$ and the $Q_i$ are taken to be elements of the Boolean domain $\mathbb{B}$.
Another, different attempt at formalizing this kind of reasoning uses the Iverson bracket. We define $$\frac{P}{Q_0,\cdots,Q_{n-1}} \iff \left([P] = \sum_{i \in \mathbb{N}_{<n}} [Q_i]\right)$$
These approaches don't quite agree. For instance, consider the expression $$\frac{\mathrm{False}}{\mathrm{True} \quad \mathrm{True}}$$ Under the first definition, its true. Under the second definition, its false.
In any event, each approach gives us a way of assigning to each natural number $n \in \mathbb{N}$ a function $$\mathbb{B} \times \mathbb{B}^n \rightarrow \mathbb{B}$$
So we get a family of such functions.

Question 0. Is there a consensus on which of these families is the 'correct' formalization?
If so, what is this family of functions called, what are the main identities/laws it satisfies, and where can I learn more about it?
Also, does anyone know of any formal proof calculi that describes how to reason with this thing?

I think we can go a lot further. If we agree to write $\sqcup$ for the coproduct of sets (also known as the "tagged union" or "discriminated union"), then the following inference rule looks very, very reasonable:
$$\frac{p:A \sqcup B}{p:A \qquad p:B}$$
This is different to what we were doing before, because now instead of dealing with booleans, we're dealing with typing judgements. Nonetheless, it seems to make sense.

Question 1. Are there any type theories that take this kind of thing seriously?

 A: This is usually formalized just as disjunctions. The initial split is by knowing that
$$ t^2=1 \to (t=1 \lor t=-1) $$
and the reasoning within each branch can then be done with metatheorems like
$$ (p\to q) \land (p\lor r) \to (q\lor r) $$
So I would say that your $\sqcup$ is simply the good old $\lor$. (In fact, for intuitionistic propositional logic, $\lor$ does correspond to tagged union under the Curry-Howard isomorphism).
Note that there's nothing in the form of the reasoning that depends on the cases being mutually exclusive -- they happen to conflict with each other, but there's nothing in the reasoning that uses this fact. The structure of the argument is exactly the same as when we split $ab=0$ into $a=0$ or $b=0$, in which the cases are not mutually exclusive.
We can also draw a parallel to classical sequent calculus, where we can derive
$$ t^2=1 \vdash t=1, t=-1 $$
because a comma on the right-hand side of the sequent is morally equivalent to a disjunction, and then work further on each of the cases "natively" within the calculus.
