proposition: Lemma ldec_conj P Q : ldec P -> ldec Q -> ldec (conj P Q).
proof: Proof. intros [u [[cls_u lam_u] decP]] [v [[cls_v lam_v] decQ]]. exists (tconj u v). unfold tconj. split. Lproc. intros s. destruct (decP s) as [b [Hu Ps]], (decQ s) as [b' [Hv Qs]];exists (andb b b'). split. - Lsimpl. rewrite Hu,Hv. now Lsimpl. - destruct b,b';simpl;unfold conj;intuition. Qed.