fact: Record computable (P : comp_pair) := { comp_norm : forall ectx t, comp_term P ectx t -> norm ectx t; comp_val_of_term : forall ectx t v, TmEval ectx t v -> comp_term P ectx t -> comp_val P v; comp_term_of_val : forall ectx t v, TmEval ectx t v -> comp_val P v -> comp_term P ectx t }.
imports: List Arith Bool