fact: Fixpoint charFunction (n : nat) : naryRel n -> naryFunc n := match n return (naryRel n -> naryFunc n) with | O => fun R : bool => match R with | true => 1 | false => 0 end | S m => fun (R : naryRel (S m)) (a : nat) => charFunction m (R a) end.
imports: Coq(Arith)