{ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} →
          {c₂ : ComplexShape ι₂} →
            {e₁ : c₁.Embedding c} → {e₂ : c₂.Embedding c} → e₁.AreComplementary e₂ → {i₂ : ι₂} → e₂.BoundaryGE i₂ → ι₁