Library Ftypesystem

Require Import Omega.
Require Import List.

Require Import list.
Require Import Flanguage.
Require Export typesystem.

Inductive jterm M : type_envcoer_envterm_envtermtypeProp :=
| JVar : H Z G k x t,
           (1 Mjterm_env M H Z G) →
           nth x G Top = t
           jterm M H Z G (Var_x k x) t
| JLam : H Z G k a t s,
           (M 1 → jtype M H Z t) →
           jterm M H Z (t :: G) a s
           jterm M H Z G (Lam k a) (Arr t s)
| JApp : H Z G k a b t s,
           jterm M H Z G a (Arr t s) →
           jterm M H Z G b t
           jterm M H Z G (App k a b) s
| JPair : H Z G k a b t s,
            jterm M H Z G a t
            jterm M H Z G b s
            jterm M H Z G (Pair k a b) (Prod t s)
| JFst : H Z G k a t s,
           jterm M H Z G a (Prod t s) →
           jterm M H Z G (Fst k a) t
| JSnd : H Z G k a t s,
           jterm M H Z G a (Prod t s) →
           jterm M H Z G (Snd k a) s
| JCoer : dH H dZ Z G a t s,
            (1 Mjterm_env M H Z G) →
            jcoer M H Z nil nil dH dZ t s
            jterm M (dH + H) (dZ ++ dmap (lift dH 0) Z) (map (lift dH 0) G) a t
            jterm M H Z G a s
.

Lemma jterm_extract_jterm_env : {M H Z G a t}, 1 M
  jterm M H Z G a tjterm_env M H Z G.
Proof.
intros M H Z G a t M1M HZGat; induction HZGat; auto.
destruct IHHZGat. inversion H2; auto.
Qed.

Lemma jterm_extract_jtype : {M H Z G a t}, 1 M
  jterm M H Z G a tjtype M H Z t.
Proof.
intros M H Z G a t M1M HZGat.
induction HZGat;
repeat (match goal with
  | H1 : 1 M_ |- _pose proof (H1 M1M); clear H1
  | |- jtype _ _ _ ?t ⇒ (is_var t; fail 1) || constructor
  | H1 : jtype _ _ _ ?t |- _ ⇒ (is_var t; fail 1) || inversion H1; clear H1
end; auto).
  destruct H2; subst; apply Forall_nth; auto; apply JTTop.
  pose proof (jterm_extract_jterm_env M1M HZGat) as [? ?].
  inversion H2; auto.
  apply (jcoer_extract_right_type M1M H1).
Qed.