proposition: Lemma proj1_prodE : proj1_chain prod_chain = [f1 ^^ proj1_chain s by M1].
proof: Proof. rewrite /proj1_chain /prod_chain !comp_chainE !/comp /=. by apply/chainE. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)