Recovering labelled parents from graph reconstructions

A reconstruction isomorphism and the old leaf labels determine the parent leaf and branching conditions. This separates graph surgery from labels.

theorem BGW.StableTrees.Marchal.exists_graft_inl_of_iso {n m : ℕ} (T : LTree (n + 1)) (G : SimpleGraph (Fin m)) (a : ↑G.edgeSet) (e : graftGraph G (Sum.inl a) ≃g T.G) (f : Fin (n + 1) ↪ Fin m) (hold : ∀ (i : Fin (n + 1)), e (f i).castSucc.castSucc = T.labels i.castSucc) (hnew : e (Fin.last (m + 1)) = T.labels (Fin.last (n + 1))) : ∃ (S : LTree n) (p : Position S.G), ⟦graft S p⟧ = ⟦T⟧

An edge-graft reconstruction with the right leaf labels gives a labelled parent.