proposition: Lemma proof (p s : syntax) : content p = content s -> forall env, eval idx op env p = eval idx op env s.
proof: Proof. suff evalE env t : eval idx op env t = \big[op/idx]_(i <- t) (pos idx env i). move=> cps e; rewrite !evalE; apply: perm_big. by apply/allP => x _ /=; rewrite !count_memE cps. elim: t => //= [n|t -> t' ->]; last by rewrite serial_Op big_cat. by rewrite big_cons big_nil Monoid.mulm1. Qed.
imports: HB(structures) BinPos BinNat mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq bigop)