P22a Full ⇒ semantic transport

Declarations: P22a_full_transport_implies_semantic

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P22a_full_transport_implies_semantic
    {A B : System} :
    FullTransport A B → SemanticTransport A B :=
  fullTransport_implies_semantic