proposition: Lemma lacc_conj P Q : lacc P -> lacc Q -> lacc (conj P Q).
proof: Proof. intros [u1 [[? ?] Hu1]] [u2 [[? ?] Hu2]]. exists (acc_conj u1 u2). split. unfold acc_conj. Lproc. intros; rewrite acc_conj_correct; firstorder. Qed.