∀ {L : FirstOrder.Language} {ι : Type u_1} [inst : Preorder ι] (G : ι → Type u_2) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) (x : FirstOrder.Language.Structure.Sigma f)
  (motive :
    (x_1 : FirstOrder.Language.Structure.Sigma f) →
      (match x_1 with
        | ⟨i, x_2⟩ =>
          match x with
          | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x_2 = (f j k jk) y) →
        Prop)
  (x_1 : FirstOrder.Language.Structure.Sigma f)
  (x_2 :
    match x_1 with
    | ⟨i, x_2⟩ =>
      match x with
      | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x_2 = (f j k jk) y),
  (∀ (fst : ι) (snd : G fst)
      (x :
        match ⟨fst, snd⟩ with
        | ⟨i, x_3⟩ =>
          match x with
          | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x_3 = (f j k jk) y),
      motive ⟨fst, snd⟩ x) →
    motive x_1 x_2