{ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      {M : Type u_4} →
        {N : Type u_5} →
          {inst : CommRing S} →
            {inst_1 : LinearOrder S} →
              {inst_2 : CommRing R} →
                {inst_3 : Algebra S R} →
                  {inst_4 : AddCommGroup M} →
                    {inst_5 : Module R M} →
                      {inst_6 : AddCommGroup N} →
                        {inst_7 : Module R N} →
                          {P : RootPairing ι R M N} →
                            {inst_8 : P.IsValuedIn S} →
                              {P_1 : Sort u} →
                                {form : LinearMap.BilinForm R M} →
                                  {symm : LinearMap.IsSymm form} →
                                    {isOrthogonal_reflection :
                                        ∀ (i : ι), LinearMap.IsOrthogonal form ⇑(P.reflection i)} →
                                      {exists_eq :
                                          ∀ (i j : ι), ∃ s, (algebraMap S R) s = (form (P.root i)) (P.root j)} →
                                        {exists_pos_eq :
                                            ∀ (i : ι), ∃ s > 0, (algebraMap S R) s = (form (P.root i)) (P.root i)} →
                                          {form' : LinearMap.BilinForm R M} →
                                            {symm' : LinearMap.IsSymm form'} →
                                              {isOrthogonal_reflection' :
                                                  ∀ (i : ι), LinearMap.IsOrthogonal form' ⇑(P.reflection i)} →
                                                {exists_eq' :
                                                    ∀ (i j : ι),
                                                      ∃ s, (algebraMap S R) s = (form' (P.root i)) (P.root j)} →
                                                  {exists_pos_eq' :
                                                      ∀ (i : ι),
                                                        ∃ s > 0, (algebraMap S R) s = (form' (P.root i)) (P.root i)} →
                                                    { form := form, symm := symm,
                                                          isOrthogonal_reflection := isOrthogonal_reflection,
                                                          exists_eq := exists_eq, exists_pos_eq := exists_pos_eq } =
                                                        { form := form', symm := symm',
                                                          isOrthogonal_reflection := isOrthogonal_reflection',
                                                          exists_eq := exists_eq', exists_pos_eq := exists_pos_eq' } →
                                                      (form ≍ form' → P_1) → P_1