fact: Definition eval(t : term): nat := let (tp, res) := interp_term nil t in match tp as t0 return (interp_type t0 -> nat) with | tpNat => fun (res: interp_type tpNat) => res | tpArr tp1 tp2 => fun (res: interp_type (tpArr tp1 tp2)) => 0 end res.
imports: Arith Lia List