add subscript exn to prim_types_program
progress on proving prim_env_inv