unsuccessful attempt to make the meta prover work;

this will require more work and more thought about how explicit
polymorphism and meta-prover should go along.