Each graph-composition operator includes its operands via an index
translation preserving node payloads and edges. Capture that once as
GGraph.Embed (a structure, not a class: for g ; g both inclusions share
the type Embed g (g <~> g), so instance resolution could pick the wrong
copy) with five named witnesses, and replace the five structurally
identical trace-lifting inductions in Properties.lean with a single
generic Trace.embed plus one-line corollaries.
The same witnesses' nodes_eq fields will back the upcoming AST-id/CFG
label bijection, so the per-operator content is stated exactly once.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Danila Fedorin
904f6375be