fact: Fixpoint nat_unenc (s : term) := match s with | lam (lam #1) => Some 0 | lam (lam (app #0 s)) => match nat_unenc s with Some n => Some (S n) | x=>x end | _ => None end.
imports: Undecidability.Shared.Libs.PSL.Numbers Nat Undecidability.L(Datatypes.LBool Functions.EqBool Datatypes.LProd)