proposition: Lemma acc_conj_correct p q s : closed p -> closed q -> (pi (acc_conj p q) s <-> pi p s /\ pi q s).
proof: Proof. intros cls_p cls_q. split. - intros [x [Hx lx]]. assert (H : converges (lam( q (enc s)) (p (enc s)))). { exists x;split;auto. symmetry. symmetry in Hx. unfold acc_conj in Hx. rewrite Hx. redStep. LsimplRed. } destruct (app_converges H) as [_ [y [Hy ly]]]. split. + eexists; split;eassumption. + exists x;split;auto. rewrite <- Hx. symmetry. clear Hx. unfold acc_conj. LsimplRed. rewrite Hy. LsimplRed. - intros [[x [Hx ?]] [y [Hy ?]]]. exists y. split. unfold acc_conj. LsimplRed. rewrite Hx. LsimplRed. tauto. Lproc. Qed.