The meta_level symbol yields appears within all proofs.