proposition: Lemma fmap_ind2 (P : fmap -> fmap -> Prop) : P nil nil -> (forall k v1 v2 s1 s2, path ord k (supp s1) -> path ord k (supp s2) -> P s1 s2 -> P (ins k v1 s1) (ins k v2 s2)) -> forall s1 s2, supp s1 =i supp s2 -> P s1 s2.
proof: Proof. move=>H1 H2; elim/fmap_ind'=>[|k1 v1 s1 T1 IH1]; elim/fmap_ind'=>[|k2 v2 s2 T2 _] //. - by move/(_ k2); rewrite supp_ins inE /= eq_refl supp_nil. - by move/(_ k1); rewrite supp_ins inE /= eq_refl supp_nil. by case/supp_eq_ins=>// E; rewrite -{k2}E in T2 *; move/IH1; apply: H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)