Thus we immediately get \((\mathtt {f},\mathtt {t}),(\mathtt {t},\mathtt {f})\in =_\mathbb {B}^\mathbf {N}\) . But this is not all, namely, if \(b_0\)  is provably a partial term i.e.,
\(\vdash b_0\lnot \equiv \mathtt {f}\wedge b_0\lnot \equiv \mathtt {t}\) , then \((b,b_0),(b_0,b)\in =_\mathbb {B}^\mathbf {N}\) . Hence, \(=_\mathbb {B}^\mathbf {N}\)  also contains all pairs of booleans where at least one of the components is partial. In the canonical model of \(\mathrm {TCF}\)  (see [1]}, Chapter 6) the strong negation \(\mathbf {K}^\mathbf {N}\)  of some inductive or coinductive predicate \(\mathbf {K}\)  can be seen as the weak complement of \(\mathbf {K}\subseteq \lbrace \vec{t}:\vec{\tau }\rbrace \) . In many situations this might be a bit too strong e.g., if we study the properties of total terms of some type then we don't want to deal with actual partial terms. In particular, proving that something is partial is usually hard. Luckily, there is some degree of freedom in the definition of \(\mathbf {K}^\mathbf {N}\) . Namely, if we specify a formula \(C\)  with \(\mathbf {K}\subseteq C\)  that characterizes the terms we are interested in, then we can define \(\mathbf {K}^\mathbf {N}_C\)  in such a way that it corresponds to the relative complement \(C\backslash \mathbf {K}\) . For a (co)inductive predicate \(\mathbf {K}\)  and a formula \(C\)  with \(\forall _{\vec{y}}(C\vec{y}\rightarrow \mathbf {K}\vec{y})\)  we define
\(\mathbf {K}_C^\mathbf {N}(\nu /\mu )_{X^{\prime }}\big (\forall _{\vec{y}}\big (C\rightarrow (\forall _{\vec{x}_i}(\vec{y}\equiv \vec{t}_i\rightarrow B_{i}))_{i<k}\rightarrow X^{\prime }\vec{y}\big )\big ).\) 

