proposition: Lemma lambdab_spec t : Bool.reflect (lambda t) (lambdab t).
proof: Proof. destruct t;constructor;[intros H;inv H;congruence..|auto]. Qed.
imports: Undecidability.L(Computability.Decidability Datatypes.LNat Datatypes.LTerm L) Nat