# Library Options

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

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

Hint Unfold some none : cbv.

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).

Proof.

crush.

Qed.

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

Proof.

destruct 1 as [cls_s [x B]], 1 as [cls_t [y D]].

rewrite B. reduction'. rewrite <- B.

rewrite D. reduction'. rewrite <- D.

crush.

Qed.

Lemma none_correct s t : lambda s -> lambda t -> none s t == t.

Proof.

intros. crush.

Qed.

Lemma some_inj s t : lambda s -> lambda t -> some s == some t -> s = t.

Proof.

intros.

eapply eqTrans with (s := lam(lam (#1 s))) in H1.

symmetry in H1. eapply eqTrans with (s := lam(lam (#1 t))) in H1.

eapply eq_lam in H1. congruence.

symmetry; now reduction'.

symmetry; now reduction'.

Qed.

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

Proof.

intros lam_v H.

symmetry in H. eapply eqTrans with (s := lam(lam(#1 v))) in H. eapply eq_lam in H. inv H. reflexivity.

symmetry; clear H; crush.

Qed.

Lemma none_equiv_some v : ~ none == some v.

Proof.

intros H. assert (converges (some v)) by (eexists; rewrite <- H; cbv; now unfold none). destruct (app_converges H0) as [_ ?]. destruct H1. rewrite H1 in H.

symmetry in H. eapply eqTrans with (s := (lam (lam (#1 (lam x))))) in H.

eapply eq_lam in H. inv H. symmetry. unfold some. clear H. crush.

Qed.