# lemma WITHOUT proof — proof.typ is absent on disk; manifest omits it from fields