Definition pi s t := converges (s (tenc t)).

Definition lacc (P : term → Prop) :=
  ∃ u, proc u ∧ ∀ t, P t ↔ pi u t.

Goal ∀ s1 s2 t, s1 == s2 → (pi s1 t ↔ pi s2 t).

Definition acc_conj (p q : term) := lam ((lam (q #1)) (p #0) ).

Lemma acc_conj_correct p q s : closed p → closed q → (pi (acc_conj p q) s ↔ pi p s ∧ pi q s).

Lemma lacc_conj P Q : lacc P → lacc Q → lacc (conj P Q).

Lemma lacc_disj M N : lacc M → lacc N → lacc (disj M N).

Lemma dec_lacc M : ldec M → lacc M.

Lemma dec_acc : ∀ M, ldec M → lacc M ∧ lacc (complement M).