∀ {L : FirstOrder.Language} {M : Type u_4} {N : Type u_3} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N) {n : ℕ} (R : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap R (⇑(FirstOrder.Language.Embedding.codRestrict f.toHom.range f ⋯) ∘ x) ↔
    FirstOrder.Language.Structure.RelMap R x