fact: Fixpoint term_to_msetcs (t: mset_term) : list msetc := match t with | mset_term_zero => [msetc_zero (term_to_nat t)] | mset_term_var x => [] | mset_term_plus u v => [msetc_sum (term_to_nat t) (term_to_nat u) (term_to_nat v)] ++ (term_to_msetcs u) ++ (term_to_msetcs v) | mset_term_h u => [msetc_h (term_to_nat t) (term_to_nat u)] ++ (term_to_msetcs u) end.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun