fact: Fixpoint evalConstFunc (n m : nat) {struct n} : naryFunc n := match n return (naryFunc n) with | O => m | S n' => fun _ => evalConstFunc n' m end.
imports: Coq(Arith Peano_dec Compare_dec List Eqdep_dec Utf8) hydras(extEqualNat misc Compat815) Coq(Lia)