Function voile::check::unify::unify_neutral

fn unify_neutral(tcs: TCS, a: &Neutral, b: &Neutral) -> TCM

Unify two neutral terms. $$ \newcommand{\casevS}[2]{\textbf{split}\ #1\ (#2)} \newcommand{\caseTr}[0]{\text{ct}} \newcommand{\clabVal}[0]{\delta} \newcommand{\caseextS}[2]{\textbf{split}\ (#1)\ \textbf{or}\ #2} \newcommand{\Gvdash}[0]{\Gamma \vdash} \newcommand{\recExt}[1]{\mid #1} \cfrac{ \Gvdash [k_0] \simeq [k_1] }{ \Gvdash [k_0 .n] \simeq [k_1 .n] \quad \cfrac{\Gvdash \{ \clabVal_0 \} \simeq \{ \clabVal_1 \}}{ \Gvdash [\{ \clabVal_0 \recExt{k_0} \}] \simeq [\{ \clabVal_1 \recExt{k_1} \}] } \quad } \\ \space \\ \cfrac{ \Gvdash \lambda c_0 \simeq \lambda c_1 \quad \Gvdash \lambda \langle \caseTr_0 \rangle \simeq \lambda \langle \caseTr_1 \rangle }{ \Gvdash \lambda \langle n\ c_0, \caseTr_0 \rangle \simeq \lambda \langle n\ c_1, \caseTr_1 \rangle } \\ \space \\ \cfrac{ \Gvdash [k_0] \simeq [k_1] \quad \Gvdash \lambda \langle \caseTr_0 \rangle \simeq \lambda \langle \caseTr_1 \rangle }{ \Gvdash [\caseextS{\caseTr_0}{k_0}] \simeq [\caseextS{\caseTr_1}{k_1}] \quad \Gvdash [\casevS{k_0}{\caseTr_0}] \simeq [\casevS{k_1}{\caseTr_1}] } $$