Theorem: Network.Graph.Path.Child.split_fst_eq_parent (Runtime/Network/Graph/Path/Child.lean)

State before:
graph✝ : Graph
a✝ : Class graph✝
path : Path graph✝ a✝
child : Child path
⊢ (split child.val (_ : isCons child.val = true)).fst = path
Tactic:
sorry
State after:
no goals