{P : Type u_1} →
  {L : Type u_2} →
    [inst : Membership P L] →
      {motive : Configuration.HasLines P L → Sort u} →
        (t : Configuration.HasLines P L) →
          ([toNondegenerate : Configuration.Nondegenerate P L] →
              (mkLine : {p₁ p₂ : P} → p₁ ≠ p₂ → L) →
                (mkLine_ax : ∀ {p₁ p₂ : P} (h : p₁ ≠ p₂), p₁ ∈ mkLine h ∧ p₂ ∈ mkLine h) →
                  motive { toNondegenerate := toNondegenerate, mkLine := mkLine, mkLine_ax := mkLine_ax }) →
            motive t