fact: Fixpoint lookup (x:X) (A:list (X*Y)) d: Y := match A with [] => d | (key,Lproc)::A => if eqb x key then Lproc else lookup x A d end.
imports: Undecidability.L.Tactics(LTactics) Undecidability.L.Datatypes(LFinType LBool LProd) Undecidability.L.Functions(EqBool)