What does this typed lambda-calculus notation mean?
Solution 1:
These are the definitions of $\nabla_A$ and $\texttt{case}$. These are freely defined constructors of type $$\nabla_A : \bot\to A$$ and $$\texttt{case} : A + B\to (A\to C) \to (B \to C) \to C.$$ They don't reduce to anything. They are simply the proof constructors corresponding to elimination of $\bot$ and $+$.