The corank induction of thm:path-theorem. This file does not import the
public target, so none of its dependencies can rely on that target.
theorem
TutteFormalization.path_theorem_induction
{α : Type u_1}
(M : Matroid α)
[M.Finite]
(Γ : Set (Set α))
(hΓ : ModularCut M Γ)
(F : Set α)
(hF : Indecomposable M F)
(X Y : Set α)
(hX : IsHyperplane M X)
(hY : IsHyperplane M Y)
(hFX : F ⊆ X)
(hFY : F ⊆ Y)
(hXoff : X ∉ Γ)
(hYoff : Y ∉ Γ)
: