apply path_class_of_contains_path
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ 𝟙 u = u ⤳[Γ] u
case hpΓ
V : Type u_1
E : Type u_2
G : Graph V E
Γ : SpanningSubtree G
u : V
⊢ Subgraph.contains Γ.toSubgraph (EdgePath.nil u)