Definition nat_twobools (n: nat) := Arity nat (Arity bool nat (2*n)) n.