proposition: Lemma oev_cat a ks1 ks2 f z0 : oeval a (ks1 ++ ks2) f z0 = oeval a ks2 f (oeval a ks1 f z0).
proof: Proof. by elim: ks1 z0=>/=. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)