typeclass - vector reflexivity under setoid equality using CoRN MathClasses -

i have simple lemma:

lemma map2_comm: forall (f:a->a->b) n (a b:t n),                     (forall x y, (f x y) = (f y x)) -> map2 f b = map2 f b a. 

which able prove using standard equality (≡). need prove similar lemma using setoid equality (using corn mathclasses). new library , type classes in general , having difficulty doing so. first attempt is:

lemma map2_setoid_comm  `{equiv b} `{equiv (t b n)} `{commutative b a}:   forall (a b: t n),     map2 f b = map2 f b a. proof.   intros.   induction n.   dep_destruct a.   dep_destruct b.   simpl. 

(here '=' 'equiv'). after 'simpl' goal "(nil b)=(nil b)" or "[]=[]" using vectornotations. finish using 'reflexivity' tactics gives me:

tactic failure: relation equiv not declared reflexive relation. maybe need require setoid library. 

i guess need somehow define reflexivity vector types, not sure how that. please advise.

first of lemma definition needs adjusted to:

lemma map2_setoid_comm : forall `{co:commutative b f} `{sb: !setoid b}  ,                   forall n:nat, commutative (map2 f (n:=n)). 

to able use reflexivity:

definition vec_equiv `{equiv a} {n}: relation (vector n) := vforall2 (n:=n) equiv. instance vec_equiv `{equiv a} {n}: equiv (vector n) := vec_equiv.