Lemma 40 ([Canonical bit and recovery proofs]). For ε∈0,1 there are proofs of the signed bit bit(emb₁(t)),, ε=1,; (emb₀(t)),, ε=0, and a proof of rec(emb_ε (t);u.Φ) ↔Φ[u:=t].

Cancel the second wrapper, then the first. Evaluation of emb_1(t) against mk_1(u.Φ) is biconditional to Φ[u:=t] ; evaluation of emb_0(t) against the same value is biconditional to Φ[u:=t] . Each comparison follows by pl from the two cancellation proofs. With Φ= , the proof of and these comparisons give the signed bits. If ε=1 , the definition of rec then selects the positive comparison. If ε=0 , it selects the negation of the negative comparison. The propositional double-negation equivalence is available from pl by Lemma 36 ([Finite propositional derivations]), since the logical constructors and classical proof builders have already been derived in the labelled fragment. Thus pl gives the recovery biconditional in both cases.