proposition: Lemma Eq_ldec : ~ ldec (fun x => exists (s t : term), x = enc (s t) /\ s == t).
proof: Proof. intros [u [[cls_u lam_u] Hu]]. pose (t := I). eapply (C27_proc (t := t)). Lproc. pose (v := (lam(u ((ext (enc (X:=term))) ((ext app) #0 (ext t)))))). exists v. split. subst v;Lproc. intros s. destruct (Hu (ext (s t))) as [b [eq C]]. exists b. split. + subst v. Lsimpl. eassumption. + destruct b. * destruct C as [? [? [eq' ?]]]. apply inj_enc in eq'. congruence. * intros eq'. apply C. now repeat eexists. Qed.