{L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] → [IsEmpty L.Constants] → [IsEmpty (L.Relations 0)] → Inhabited (L.FGEquiv M N)