proposition: Lemma self_div_comb : ~ lacc self_diverging_comb.
proof: Proof. intros [u [[cls_u lam_u] H]]. unfold self_diverging_comb in H. unfold conj in H. specialize (H u). unfold self_diverging in H. destruct H. unfold proc in *. tauto. Qed.