Definition none : term := .\"s", "n"; "n".
Definition some : term := .\"t", "s", "n"; "s" "t".


Definition oenc t :=
  match t with
  | Some t ⇒ lam(lam (#1 (tenc t)))
  | None ⇒ none
  end.

Lemma some_correct_enc s : some (tenc s) == oenc (Some s).

Lemma some_correct s t u: proc s → proc t → (some s) t (lam u) == t s.

Lemma none_correct s t : lambda s → lambda t → none s t == t.

Lemma some_inj s t : lambda s → lambda t → some s == some t → s = t.

Lemma oenc_correct_some (s v : term) : lambda v → oenc (Some s) == some v → v == tenc s.

Lemma none_equiv_some v : ¬ none == some v.