∀ (L : FirstOrder.Language) (M : Type u_3) [inst : L.Structure M] {n : ℕ} (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r ((Function.Embedding.refl M).toFun ∘ x) ↔
    FirstOrder.Language.Structure.RelMap r x