Constant CERT_ACCEPTED_ARTIFACT 

pub const CERT_ACCEPTED_ARTIFACT: &str = "-- Lean-side artifact acceptance shim.\n--\n-- The dependency-closed acceptance machinery lives in\n-- `AcceptedArtifactCore.lean`; this shim adds the one conjunction that uses\n-- the Module-dependent `Schema.Holds` proposition.\nimport Schema\nimport AcceptedArtifactCore\nimport ClaimAxes\nimport StandardFace\n\nnamespace AverCert.AcceptedArtifact\n\ndef accepted (artifact : ArtifactData) : Prop :=\n  AverCert.Schema.Holds artifact.manifest \u{2227}\n  subjectMatchesArtifactRoot artifact \u{2227}\n  fragmentClaimObligationsInManifest artifact \u{2227}\n  claimsMatchManifest artifact \u{2227}\n  AverCert.StandardFace.checkedFaces artifact \u{2227}\n  AverCert.ClaimAxes.checked artifact = true \u{2227}\n  decodedNonExprFacts artifact \u{2227}\n  acceptedFragments artifact\n\nend AverCert.AcceptedArtifact\n";