proposition: Lemma iter_ind C : (forall x y, R x y -> C x -> C y) -> forall x y, iter R x y -> C x -> C y.
proof: Proof. move=>H x y /(@iterf_ind (fun => True) (fun x y => C x -> C y)). by apply=>// t1 t2 /H X _. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)