Require Import PeanoNat List.
Import ListNotations.

Definition mset_eq (A B: list ) : Prop :=
   c, count_occ Nat.eq_dec A c = count_occ Nat.eq_dec B c.
Local Notation "A ≡ B" := (mset_eq A B) (at level 65).

Inductive msetc : Set :=
  | msetc_zero : msetc
  | msetc_sum : msetc
  | msetc_h : msetc.

Definition msetc_sem (φ: list ) (c: msetc) :=
  match c with
    | msetc_zero x φ x [0]
    | msetc_sum x y z φ x (φ y) (φ z)
    | msetc_h x y φ x map S (φ y)
  end.

Definition FMsetC_SAT (l : list msetc) := φ, c, In c l msetc_sem φ c.