fact: Definition eval_f (t : term) (ty : type)(well_typed : TyRel [] t ty) : value := let triple := {| red_ctx := [::]; red_tm := t; red_correct := norm_f t ty well_typed |} in let v := eval_triple triple in proj1_sig v.
imports: List Arith Bool Wellfounded