fact: Definition encode_eq (t u: mset_term) := [(msetc_sum 0 0 0); (msetc_sum (term_to_nat t) 0 (term_to_nat u))].
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun