fact: Definition unembed n := let (xy, z) := Cantor.of_nat n in (Cantor.of_nat xy, z).
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun