proposition: Lemma iter2 A T (g : A -> T -> A -> T -> Prop) x1 s1 x2 s2 : g x1 s1 x2 s2 -> iterc g x1 s1 x2 s2.
proof: Proof. by apply: iter1. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)