coq - Morphism - 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.