qed.
(* Inversion lemmas with iterated next **************************************)
lemma isdiv_inv_nexts: ān,g. šāŖā*[n]gā« ā šāŖgā«.
qed.
(* Inversion lemmas with iterated next **************************************)
lemma isdiv_inv_nexts: ān,g. šāŖā*[n]gā« ā šāŖgā«.