∀ {L : FirstOrder.Language} {G' : ℕ → Type w} [inst : (i : ℕ) → L.Structure (G' i)]
  (f' : (n : ℕ) → L.Embedding (G' n) (G' (n + 1))) (m n : ℕ) (h : m ≤ n),
  ⇑(FirstOrder.Language.DirectedSystem.natLERec f' m n h) = fun a => Nat.leRecOn h (fun k => ⇑(f' k)) a