Require Import PeanoNat List.
Import ListNotations.

Definition mset_eq (A B: list nat) : Prop :=
  forall 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 : nat -> msetc
  | msetc_sum : nat -> nat -> nat -> msetc
  | msetc_h : nat -> nat -> msetc.

Definition msetc_sem (φ: nat -> list nat) (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) := exists φ, forall c, In c l -> msetc_sem φ c.