proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);