fact: Definition raw_add_nodefault (k:key) (x:elt) (l:Raw.farray key elt) := if cmp x default_value then if Raw.mem key_comp k l then Raw.remove key_comp k l else l else Raw.add key_comp k x l.
imports: Bool OrderedType SMT_classes ProofIrrelevance