Record Disjointness

$$\infer{\Gamma \vdash c_1 \sim c_2}{ \Gamma \vdash c_1 \hookright... ...mma \vdash c'_1 \sim c'_2 } \quad \infer{\Gamma \vdash X \sim X'}{ X \neq X' }$$

$$\infer{\Gamma \vdash c_1 \sim c_2}{ c'_1 \sim c'_2 \in \Gamma &... ...w C_1 & \Gamma \vdash c'_2 \hookrightarrow C_2 & c_1 \in C_1 & c_2 \in C_2 }$$

$$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{} \quad \infer{\Gam... ...\mathsf{map} \; f \; c \hookrightarrow C}{ \Gamma \vdash c \hookrightarrow C }$$