{P : Type u_1} →
  {L : Type u_2} →
    {inst : Membership P L} →
      {P_1 : Sort u} →
        {toNondegenerate : Configuration.Nondegenerate P L} →
          {mkPoint : {l₁ l₂ : L} → l₁ ≠ l₂ → P} →
            {mkPoint_ax : ∀ {l₁ l₂ : L} (h : l₁ ≠ l₂), mkPoint h ∈ l₁ ∧ mkPoint h ∈ l₂} →
              {toNondegenerate' : Configuration.Nondegenerate P L} →
                {mkPoint' : {l₁ l₂ : L} → l₁ ≠ l₂ → P} →
                  {mkPoint_ax' : ∀ {l₁ l₂ : L} (h : l₁ ≠ l₂), mkPoint' h ∈ l₁ ∧ mkPoint' h ∈ l₂} →
                    { toNondegenerate := toNondegenerate, mkPoint := mkPoint, mkPoint_ax := mkPoint_ax } =
                        { toNondegenerate := toNondegenerate', mkPoint := mkPoint', mkPoint_ax := mkPoint_ax' } →
                      (mkPoint ≍ mkPoint' → P_1) → P_1