Function double_check 

pub fn double_check(ctx: &Context, term: &Term) -> DoubleCheck

Cross-check term against both infer_type and recheck.

The de Bruijn criterion in action: a proof term is most trustworthy when two independently-written kernels, on different representations, agree on its type. Disagreement is surfaced loudly; an incomplete re-check (the Fix fragment) is surfaced honestly rather than dressed up as agreement.