proposition: Lemma embed_unembed {xyz} : unembed (embed xyz) = xyz.
proof: Proof. case: xyz. case. move=> >. by rewrite /embed /unembed ?Cantor.cancel_of_to. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun