∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'}
  [inst : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)]
  [inst_1 : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)],
  ϕ.Injective → ∀ (M : Type u_1) [inst_2 : Inhabited M] [inst_3 : L.Structure M], ϕ.IsExpansionOn M