∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} {T : ⦃i j : ι⦄ → i ≤ j → Type u_3}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : (i : ι) → One (G i)] (x : (i : ι) × G i) (motive : (∃ i, ∃ (h : x.fst ≤ i), (f x.fst i h) x.snd = 1) → Prop)
  (x_1 : ∃ i, ∃ (h : x.fst ≤ i), (f x.fst i h) x.snd = 1),
  (∀ (i : ι) (h : x.fst ≤ i) (eq : (f x.fst i h) x.snd = 1), motive ⋯) → motive x_1