inductive path :: "('m ⇒ 'w list ⇒ bool) ⇒ 'w ⇒ 'w list set "
  for Rf w
  where
   "[w] ∈ path Rf w"
 | "⟦wl ∈ path Rf w ; Rf m (last wl # vl); v ∈ list.set vl⟧ ⟹ wl @ [v] ∈ path Rf w "

Proofs for inductive predicate(s) "path"
Ill-formed introduction rule ""
w0 = w ⟹ [w0] ∈ path Rf w
Conclusion of introduction rule must be an inductive predicate