proposition: Lemma ldec_complement P : ldec P -> ldec (complement P).
proof: Proof. intros [u [[cls_u lam_u] H]]. exists (tcompl u). unfold tcompl. split. Lproc. intros s. destruct (H s) as [b [A Ps]];exists (negb b). split. - Lsimpl. rewrite A. now Lsimpl. - destruct b;simpl; intuition. Qed.