proposition: Lemma size_store_aux s i x : size (@store_aux A s i x) = size s.
proof: Proof. elim: s i => [|a s IHs] i; first by case: i. case: i IHs => [|i] IHs //=. by rewrite -(IHs i). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype bigop matrix) CoqEAL(hrel param refinements seqmx seqpoly) Equivalence RelationClasses Morphisms