∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (S : Set (RingCon R)) (r : Setoid R)
  (motive : r ∈ (fun x => x.toSetoid) '' S → Prop) (x : r ∈ (fun x => x.toSetoid) '' S),
  (∀ (c : RingCon R) (hS : c ∈ S) (hr : (fun x => x.toSetoid) c = r), motive ⋯) → motive x