coq - モーフィズム - Coq の非変換項の Setoid

Question

Coqには次の機能があります。ここで、以下のようにインスタンスを定義したいと思います。私の場合、型 [nat] の等価性 [==] は定義されていますが、[StringMap.t String.t] では定義されていません。Instace SC_Proper を解決してください。ありがとう。

Definition SC (u: nat) (zm: StringMap.t String.t):
  StringMap.t String.t :=
 match u with
 | S p =>   match p with  
                 | 2  => zm 
                 | _ => 
                      match StringMap.find "S" zm with
                      | Some k => StringMap.empty 
                      | _ => zm  
                      end
                end
  | O => zm
 end.


 Instance SC_Proper 
 : Proper (equiv ==> equiv ==> equiv) SC.
Proof with o.
 repeat red. intros u u' Hu zm1 zm2 Hzm.
Admitted.