Definitional Equality

We use $\mathcal C$ to stand for a one-hole context that, when filled, yields a constructor. The notation $\mathcal C[c]$ plugs $c$ into $\mathcal C$ . We omit the standard definition of one-hole contexts. We write $[x \mapsto c_1]c_2$ for capture-avoiding substitution of $c_1$ for $x$ in $c_2$ , with analogous notation for substituting a kind in a constructor.

$$\infer{\Gamma \vdash c \equiv c}{} \quad \infer{\Gamma \vdash c_1... ...\vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{ \Gamma \vdash c_1 \equiv c_2 }$$

$$\infer{\Gamma \vdash x \equiv c}{ x :: \kappa = c \in \Gamma } \... ... \; x) = (\kappa, c) } \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$

$$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \e... ...fer{\Gamma \vdash (X \Longrightarrow c) [\kappa] \equiv [X \mapsto \kappa] c}{}$$

$$\infer{\Gamma \vdash c_1 + \hspace{-.075in} + \;c_2 \equiv c_2 + ... ... + \;c_3) \equiv (c_1 + \hspace{-.075in} + \;c_2) + \hspace{-.075in} + \;c_3}{}$$

$$\infer{\Gamma \vdash [] + \hspace{-.075in} + \;c \equiv c}{} \qua... ...\overline{c_2 = c'_2}] \equiv [\overline{c_1 = c'_1}, \overline{c_2 = c'_2}]}{}$$

$$\infer{\Gamma \vdash \mathsf{map} \; f \; [] \equiv []}{} \quad \... ...+ \;c) \equiv [c_1 = f \; c_2] + \hspace{-.075in} + \;\mathsf{map} \; f \; c}{}$$

$$\infer{\Gamma \vdash \mathsf{map} \; (\lambda x \Rightarrow x) \;... ...f' \; c) \equiv \mathsf{map} \; (\lambda x \Rightarrow f \; (f' \; x)) \; c}{}$$

$$\infer{\Gamma \vdash \mathsf{map} \; f \; (c_1 + \hspace{-.075in}... ...uiv \mathsf{map} \; f \; c_1 + \hspace{-.075in} + \;\mathsf{map} \; f \; c_2}{}$$