fact: Structure mixin_of (T : Type) := Mixin { defined_op : T -> bool; empty_op : T; undef_op : T; upd_op : K -> V -> T -> T; dom_op : T -> seq K; dom_eq_op : T -> T -> bool; assocs_op : T -> seq (K * V); free_op : T -> K -> T; find_op : K -> T -> option V; union_op : T -> T -> T; empb_op : T -> bool; undefb_op : T -> bool; pts_op : K -> V -> T; from_op : T -> UM.base C V; to_op : UM.base C V -> T; _ : forall b, from_op (to_op b) = b; _ : forall f, to_op (from_op f) = f; _ : forall f, defined_op f = UM.valid (from_op f); _ : undef_op = to_op (UM.Undef C V); _ : empty_op = to_op (UM.empty C V); _ : forall k v f, upd_op k v f = to_op (UM.upd k v (from_op f)); _ : forall f, dom_op f = UM.dom (from_op f); _ : forall f1 f2, dom_eq_op f1 f2 = UM.dom_eq (from_op f1) (from_op f2); _ : forall f, assocs_op f = UM.assocs (from_op f); _ : forall f k, free_op f k = to_op (UM.free (from_op f) k); _ : forall k f, find_op k f = UM.find k (from_op f); _ : forall f1 f2, union_op f1 f2 = to_op (UM.union (from_op f1) (from_op f2)); _ : forall f, empb_op f = UM.empb (from_op f); _ : forall f, undefb_op f = UM.undefb (from_op f); _ : forall k v, pts_op k v = to_op (UM.pts C k v)}.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)