proposition: Theorem eval_f_correct : forall t ty wt, TmEval [::] t (eval_f t ty wt).
proof: Proof. unfold eval_f. intros. pose (v := (eval_triple {| red_ctx := [::]; red_tm := t; red_correct := norm_f t ty wt |})). assert (h := @proj2_sig _ _ v). simpl in h. apply h. Qed.
imports: List Arith Bool Wellfounded