proposition: Lemma unenc_correct m : (nat_unenc (nat_enc m)) = Some m.
proof: Proof. induction m; simpl; now try rewrite IHm. Qed.
imports: Undecidability.Shared.Libs.PSL.Numbers Nat Undecidability.L(Datatypes.LBool Functions.EqBool Datatypes.LProd)