Library MoreAcc

Lemma totality : ¬ lacc(fun s ⇒ ∀ t, pi s t).

Lemma totality_proc : ¬ lacc (fun s ⇒ proc s ∧ ¬ ∀ t, pi s t).

Lemma totality_compl : ¬ (lacc (fun s ⇒ ¬ ∀ t, pi s t)).