Require Import MyTactics.
Require Import Sequences.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.
Require Import SystemFDefinition.

A size-indexed typing judgement for terms

This typing judgement is indexed with an integer n which counts the number of outstanding type abstractions and type applications, that is, the number of type abstractions and type applications that are not buried under a syntax-directed typing rule.

This integer index is used in the proof of the type substitution lemma jtn_ty_substitution, where we prove that n is preserved, and in the proof of the inversion lemma invert_jtn_Lam_TyFun, which is carried out by induction over n.

Inductive jtn : nat -> tyenv -> term -> ty -> Prop :=
| JTNVar:
    forall Gamma x T,
    Gamma x = T ->
    jtn 0 Gamma (Var x) T
| JTNLam:
    forall n Gamma t T U,
    jtn n (T .: Gamma) t U ->
    jtn 0 Gamma (Lam t) (TyFun T U)
| JTNApp:
    forall n1 n2 Gamma t1 t2 T U,
    jtn n1 Gamma t1 (TyFun T U) ->
    jtn n2 Gamma t2 T ->
    jtn 0 Gamma (App t1 t2) U
| JTNTyAbs:
    forall n Gamma Gamma' t T,
    jtn n Gamma' t T ->
    Gamma' = Gamma >> ren (+1) ->
    jtn (S n) Gamma t (TyAll T)
| JTNTyApp:
    forall n Gamma t T U T',
    jtn n Gamma t (TyAll T) ->
    T' = T.[U/] ->
    jtn (S n) Gamma t T'
.

The following hint allows eauto with jtn to apply the above typing rules.

Global Hint Constructors jtn : jtn.

Equivalence between the typing judgements

It is convenient to define a simpler typing judgement which is not indexed with an integer n. We use this judgement when we do not care about n.

Definition jt Gamma t T :=
  exists n,
  jtn n Gamma t T.

The following hint allows eauto with jt to exploit the fact that j n Gamma t T implies jt Gamma t T.

Global Hint Unfold jt : jt.

It is convenient to reformulate the typing rules at the level of jt. This is somewhat redundant, but nothing complicated is going on here.

Lemma JTVar:
  forall Gamma x T,
  Gamma x = T ->
  jt Gamma (Var x) T.forall (Gamma : var -> ty) (x : var) (T : ty),
Gamma x = T -> jt Gamma (Var x) T
Proof.forall (Gamma : var -> ty) (x : var) (T : ty),
Gamma x = T -> jt Gamma (Var x) T
  unfold jt.forall (Gamma : var -> ty) (x : var) (T : ty),
Gamma x = T -> exists n : nat, jtn n Gamma (Var x) T intros.Gamma: var -> ty
x: var
T: ty
H: Gamma x = T
exists n : nat, jtn n Gamma (Var x) T unpack.Gamma: var -> ty
x: var
exists n : nat, jtn n Gamma (Var x) (Gamma x) eauto using jtn.
Qed.

Lemma JTLam:
  forall Gamma t T U,
  jt (T .: Gamma) t U ->
  jt Gamma (Lam t) (TyFun T U).forall (Gamma : var -> ty) (t : term) (T U : ty),
jt (T .: Gamma) t U -> jt Gamma (Lam t) (TyFun T U)
Proof.forall (Gamma : var -> ty) (t : term) (T U : ty),
jt (T .: Gamma) t U -> jt Gamma (Lam t) (TyFun T U)
  unfold jt.forall (Gamma : var -> ty) (t : term) (T U : ty),
(exists n : nat, jtn n (T .: Gamma) t U) ->
exists n : nat, jtn n Gamma (Lam t) (TyFun T U) intros.Gamma: var -> ty
t: term
T, U: ty
H: exists n : nat, jtn n (T .: Gamma) t U
exists n : nat, jtn n Gamma (Lam t) (TyFun T U) unpack.Gamma: var -> ty
t: term
T, U: ty
x: nat
H: jtn x (T .: Gamma) t U
exists n : nat, jtn n Gamma (Lam t) (TyFun T U) eauto using jtn.
Qed.

Lemma JTApp:
  forall Gamma t1 t2 T U,
  jt Gamma t1 (TyFun T U) ->
  jt Gamma t2 T ->
  jt Gamma (App t1 t2) U.forall (Gamma : tyenv) (t1 t2 : term) (T U : ty),
jt Gamma t1 (TyFun T U) ->
jt Gamma t2 T -> jt Gamma (App t1 t2) U
Proof.forall (Gamma : tyenv) (t1 t2 : term) (T U : ty),
jt Gamma t1 (TyFun T U) ->
jt Gamma t2 T -> jt Gamma (App t1 t2) U
  unfold jt.forall (Gamma : tyenv) (t1 t2 : term) (T U : ty),
(exists n : nat, jtn n Gamma t1 (TyFun T U)) ->
(exists n : nat, jtn n Gamma t2 T) ->
exists n : nat, jtn n Gamma (App t1 t2) U intros.Gamma: tyenv
t1, t2: term
T, U: ty
H: exists n : nat, jtn n Gamma t1 (TyFun T U)
H0: exists n : nat, jtn n Gamma t2 T
exists n : nat, jtn n Gamma (App t1 t2) U unpack.Gamma: tyenv
t1, t2: term
T, U: ty
x0: nat
H: jtn x0 Gamma t1 (TyFun T U)
x: nat
H0: jtn x Gamma t2 T
exists n : nat, jtn n Gamma (App t1 t2) U eauto using jtn.
Qed.

Lemma JTTyAbs:
  forall Gamma Gamma' t T,
  jt Gamma' t T ->
  Gamma' = Gamma >> ren (+1) ->
  jt Gamma t (TyAll T).forall (Gamma : var -> ty) (Gamma' : tyenv) (t : term)
  (T : ty),
jt Gamma' t T ->
Gamma' = Gamma >> ren (+1) -> jt Gamma t (TyAll T)
Proof.forall (Gamma : var -> ty) (Gamma' : tyenv) (t : term)
  (T : ty),
jt Gamma' t T ->
Gamma' = Gamma >> ren (+1) -> jt Gamma t (TyAll T)
  unfold jt.forall (Gamma : var -> ty) (Gamma' : tyenv) (t : term)
  (T : ty),
(exists n : nat, jtn n Gamma' t T) ->
Gamma' = Gamma >> ren (+1) ->
exists n : nat, jtn n Gamma t (TyAll T) intros.Gamma: var -> ty
Gamma': tyenv
t: term
T: ty
H: exists n : nat, jtn n Gamma' t T
H0: Gamma' = Gamma >> ren (+1)
exists n : nat, jtn n Gamma t (TyAll T) unpack.Gamma: var -> ty
t: term
T: ty
x: nat
H: jtn x (Gamma >> ren (+1)) t T
exists n : nat, jtn n Gamma t (TyAll T) eauto using jtn.
Qed.

Lemma JTTyApp:
  forall Gamma t T U T',
  jt Gamma t (TyAll T) ->
  T' = T.[U/] ->
  jt Gamma t T'.forall (Gamma : tyenv) (t : term) (T U T' : {bind ty}),
jt Gamma t (TyAll T) -> T' = T.[U/] -> jt Gamma t T'
Proof.forall (Gamma : tyenv) (t : term) (T U T' : {bind ty}),
jt Gamma t (TyAll T) -> T' = T.[U/] -> jt Gamma t T'
  unfold jt.forall (Gamma : tyenv) (t : term) (T U T' : {bind ty}),
(exists n : nat, jtn n Gamma t (TyAll T)) ->
T' = T.[U/] -> exists n : nat, jtn n Gamma t T' intros.Gamma: tyenv
t: term
T, U, T': {bind ty}
H: exists n : nat, jtn n Gamma t (TyAll T)
H0: T' = T.[U/]
exists n : nat, jtn n Gamma t T' unpack.Gamma: tyenv
t: term
T, U: {bind ty}
x: nat
H: jtn x Gamma t (TyAll T)
exists n : nat, jtn n Gamma t T.[U/] eauto using jtn.
Qed.

The following hint allows eauto with jt to use the above lemmas.

Global Hint Resolve JTVar JTLam JTApp JTTyAbs JTTyApp : jt.

The judgements jt and jf are equivalent. So, we have just given an alternate definition of System F.

Lemma jtn_jf:
  forall n Gamma t T,
  jtn n Gamma t T ->
  jf Gamma t T.forall (n : nat) (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T -> jf Gamma t T
Proof.forall (n : nat) (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T -> jf Gamma t T
  induction 1; intros; subst; eauto with jf.
Qed.

Lemma jt_jf:
  forall Gamma t T,
  jt Gamma t T ->
  jf Gamma t T.forall (Gamma : tyenv) (t : term) (T : ty),
jt Gamma t T -> jf Gamma t T
Proof.forall (Gamma : tyenv) (t : term) (T : ty),
jt Gamma t T -> jf Gamma t T
  unfold jt.forall (Gamma : tyenv) (t : term) (T : ty),
(exists n : nat, jtn n Gamma t T) -> jf Gamma t T intros.Gamma: tyenv
t: term
T: ty
H: exists n : nat, jtn n Gamma t T
jf Gamma t T unpack.Gamma: tyenv
t: term
T: ty
x: nat
H: jtn x Gamma t T
jf Gamma t T eauto using jtn_jf.
Qed.

Lemma jf_jt:
  forall Gamma t T,
  jf Gamma t T ->
  jt Gamma t T.forall (Gamma : tyenv) (t : term) (T : ty),
jf Gamma t T -> jt Gamma t T
Proof.forall (Gamma : tyenv) (t : term) (T : ty),
jf Gamma t T -> jt Gamma t T
  induction 1; intros; subst; eauto with jt.
Qed.

Substitutions of types for type variables

The typing judgement jtn is preserved by a type substitution theta, which maps type variables to types.

We prove that the measure n is preserved by such a substitution. This is required in the proof of invert_jtn_Lam_TyFun, where we apply a substitution to the type derivation before exploiting the induction hypothesis.

Lemma jtn_ty_substitution:
  forall n Gamma t T,
  jtn n Gamma t T ->
  forall Gamma' T' theta,
  Gamma' = Gamma >> theta ->
  T' = T.[theta] ->
  jtn n Gamma' t T'.forall (n : nat) (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall (Gamma' : var -> ty) (T' : ty)
  (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
Proof.forall (n : nat) (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall (Gamma' : var -> ty) (T' : ty)
  (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
  (* A detailed proof, where every case is dealt with explicitly: *)
  induction 1; intros; subst.Gamma: var -> ty
x: var
theta: var -> ty
jtn 0 (Gamma >> theta) (Var x) (Gamma x).[theta]
n: nat
Gamma: var -> ty
t: term
T, U: ty
H: jtn n (T .: Gamma) t U
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = T .: Gamma >> theta ->
T' = U.[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn 0 (Gamma >> theta) (Lam t) (TyFun T U).[theta]
n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
jtn 0 (Gamma >> theta) (App t1 t2) U.[theta]
n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn (S n) (Gamma >> theta) t (TyAll T).[theta]
n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn (S n) (Gamma >> theta) t T.[U/].[theta]
  (* JTNVar *)
  {Gamma: var -> ty
x: var
theta: var -> ty
jtn 0 (Gamma >> theta) (Var x) (Gamma x).[theta] econstructor.Gamma: var -> ty
x: var
theta: var -> ty
(Gamma >> theta) x = (Gamma x).[theta] autosubst. }n: nat
Gamma: var -> ty
t: term
T, U: ty
H: jtn n (T .: Gamma) t U
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = T .: Gamma >> theta ->
T' = U.[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn 0 (Gamma >> theta) (Lam t) (TyFun T U).[theta]
n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
jtn 0 (Gamma >> theta) (App t1 t2) U.[theta]
n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn (S n) (Gamma >> theta) t (TyAll T).[theta]
n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn (S n) (Gamma >> theta) t T.[U/].[theta]
  (* JTNLam *)
  {n: nat
Gamma: var -> ty
t: term
T, U: ty
H: jtn n (T .: Gamma) t U
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = T .: Gamma >> theta ->
T' = U.[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn 0 (Gamma >> theta) (Lam t) (TyFun T U).[theta] econstructor.n: nat
Gamma: var -> ty
t: term
T, U: ty
H: jtn n (T .: Gamma) t U
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = T .: Gamma >> theta ->
T' = U.[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn ?n (T.[theta] .: Gamma >> theta) t U.[theta] eapply IHjtn.n: nat
Gamma: var -> ty
t: term
T, U: ty
H: jtn n (T .: Gamma) t U
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = T .: Gamma >> theta ->
T' = U.[theta] -> jtn n Gamma' t T'
theta: var -> ty
T.[theta] .: Gamma >> theta = T .: Gamma >> ?theta
n: nat
Gamma: var -> ty
t: term
T, U: ty
H: jtn n (T .: Gamma) t U
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = T .: Gamma >> theta ->
T' = U.[theta] -> jtn n Gamma' t T'
theta: var -> ty
U.[theta] = U.[?theta]
      eauto with autosubst.n: nat
Gamma: var -> ty
t: term
T, U: ty
H: jtn n (T .: Gamma) t U
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = T .: Gamma >> theta ->
T' = U.[theta] -> jtn n Gamma' t T'
theta: var -> ty
U.[theta] = U.[theta]
      eauto. }n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
jtn 0 (Gamma >> theta) (App t1 t2) U.[theta]
n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn (S n) (Gamma >> theta) t (TyAll T).[theta]
n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn (S n) (Gamma >> theta) t T.[U/].[theta]
  (* JTNApp *)
  {n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
jtn 0 (Gamma >> theta) (App t1 t2) U.[theta] econstructor.n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
jtn ?n1 (Gamma >> theta) t1 (TyFun ?T U.[theta])
n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
jtn ?n2 (Gamma >> theta) t2 ?T
      eapply IHjtn1.n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
Gamma >> theta = Gamma >> ?theta
n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
TyFun ?T U.[theta] = (TyFun T U).[?theta]
n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
jtn ?n2 (Gamma >> theta) t2 ?T
        eauto.n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
TyFun ?T U.[theta] = (TyFun T U).[theta]
n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
jtn ?n2 (Gamma >> theta) t2 ?T
        asimpl.n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
TyFun ?T U.[theta] = TyFun T.[theta] U.[theta]
n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
jtn ?n2 (Gamma >> theta) t2 ?T eauto.n1, n2: nat
Gamma: tyenv
t1, t2: term
T, U: ty
H: jtn n1 Gamma t1 (TyFun T U)
H0: jtn n2 Gamma t2 T
IHjtn1: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyFun T U).[theta] ->
jtn n1 Gamma' t1 T'
IHjtn2: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n2 Gamma' t2 T'
theta: var -> ty
jtn ?n2 (Gamma >> theta) t2 T.[theta]
      eauto. }n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn (S n) (Gamma >> theta) t (TyAll T).[theta]
n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn (S n) (Gamma >> theta) t T.[U/].[theta]
  (* JTNTyAbs *)
  {n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn (S n) (Gamma >> theta) t (TyAll T).[theta] econstructor.n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn n ?Gamma' t T.[up theta]
n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
?Gamma' = Gamma >> theta >> ren (+1)
      eapply IHjtn.n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
?Gamma' = Gamma >> ren (+1) >> ?theta
n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
T.[up theta] = T.[?theta]
n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
?Gamma' = Gamma >> theta >> ren (+1)
        eauto.n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
T.[up theta] = T.[?theta]
n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
Gamma >> ren (+1) >> ?theta =
Gamma >> theta >> ren (+1)
        eauto.n: nat
Gamma: var -> ty
t: term
T: ty
H: jtn n (Gamma >> ren (+1)) t T
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> ren (+1) >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
theta: var -> ty
Gamma >> ren (+1) >> up theta =
Gamma >> theta >> ren (+1)
      autosubst. }n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn (S n) (Gamma >> theta) t T.[U/].[theta]
  (* JTNTyApp *)
  {n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn (S n) (Gamma >> theta) t T.[U/].[theta] econstructor.n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
jtn n (Gamma >> theta) t (TyAll ?T)
n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
T.[U/].[theta] = ?T.[?U/]
      eapply IHjtn.n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
Gamma >> theta = Gamma >> ?theta
n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
TyAll ?T = (TyAll T).[?theta]
n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
T.[U/].[theta] = ?T.[?U/]
        eauto.n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
TyAll ?T = (TyAll T).[theta]
n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
T.[U/].[theta] = ?T.[?U/]
        autosubst.n: nat
Gamma: tyenv
t: term
T, U: {bind ty}
H: jtn n Gamma t (TyAll T)
IHjtn: forall (Gamma' : var -> ty) 
  (T' : ty) (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = (TyAll T).[theta] -> jtn n Gamma' t T'
theta: var -> ty
T.[U/].[theta] = T.[up theta].[?U/]
      autosubst. }
Restart.forall (n : nat) (Gamma : tyenv) (t : term) (T : ty),
jtn n Gamma t T ->
forall (Gamma' : var -> ty) (T' : ty)
  (theta : var -> ty),
Gamma' = Gamma >> theta ->
T' = T.[theta] -> jtn n Gamma' t T'
  (* A shorter script, where all cases are dealt with uniformly: *)
  induction 1; intros; subst;
  econstructor; eauto with autosubst.
Qed.

As a corollary, if the term t has type T under a type environment that extends Gamma with one type variable, then for every type U, the term t has type T.[U/] under Gamma.

Again, the measure n is preserved by this substitution.

Lemma jtn_ty_substitution_0:
  forall n Gamma t T U,
  jtn n (Gamma >> ren (+1)) t T ->
  jtn n Gamma t T.[U/].forall (n : nat) (Gamma : var -> ty) (t : term)
  (T U : ty),
jtn n (Gamma >> ren (+1)) t T -> jtn n Gamma t T.[U/]
Proof.forall (n : nat) (Gamma : var -> ty) (t : term)
  (T U : ty),
jtn n (Gamma >> ren (+1)) t T -> jtn n Gamma t T.[U/]
  intros.n: nat
Gamma: var -> ty
t: term
T, U: ty
H: jtn n (Gamma >> ren (+1)) t T
jtn n Gamma t T.[U/]
  eapply jtn_ty_substitution; eauto.n: nat
Gamma: var -> ty
t: term
T, U: ty
H: jtn n (Gamma >> ren (+1)) t T
Gamma = Gamma >> ren (+1) >> U .: ids
  autosubst.
Qed.

As a corollary, the same properties hold of the judgement jf.

Lemma jf_ty_substitution:
  forall Gamma t T theta,
  jf Gamma t T ->
  jf (Gamma >> theta) t T.[theta].forall (Gamma : tyenv) (t : term) (T : ty)
  (theta : var -> ty),
jf Gamma t T -> jf (Gamma >> theta) t T.[theta]
Proof.forall (Gamma : tyenv) (t : term) (T : ty)
  (theta : var -> ty),
jf Gamma t T -> jf (Gamma >> theta) t T.[theta]
  intros.Gamma: tyenv
t: term
T: ty
theta: var -> ty
H: jf Gamma t T
jf (Gamma >> theta) t T.[theta]
  forward jf_jt.Gamma: tyenv
t: term
T: ty
theta: var -> ty
H: jf Gamma t T
H0: jt Gamma t T
jf (Gamma >> theta) t T.[theta]
  unfold jt in *.Gamma: tyenv
t: term
T: ty
theta: var -> ty
H: jf Gamma t T
H0: exists n : nat, jtn n Gamma t T
jf (Gamma >> theta) t T.[theta] unpack.Gamma: tyenv
t: term
T: ty
theta: var -> ty
H: jf Gamma t T
x: nat
H0: jtn x Gamma t T
jf (Gamma >> theta) t T.[theta]
  forward jtn_ty_substitution.Gamma: tyenv
t: term
T: ty
theta: var -> ty
H: jf Gamma t T
x: nat
H0: jtn x Gamma t T
H1: jtn x (Gamma >> ?Goal) t T.[?Goal]
jf (Gamma >> theta) t T.[theta]
  eauto using jtn_jf.
Qed.

Lemma jf_ty_substitution_0:
  forall Gamma t T U,
  jf (Gamma >> ren (+1)) t T ->
  jf Gamma t T.[U/].forall (Gamma : var -> ty) (t : term) (T U : ty),
jf (Gamma >> ren (+1)) t T -> jf Gamma t T.[U/]
Proof.forall (Gamma : var -> ty) (t : term) (T U : ty),
jf (Gamma >> ren (+1)) t T -> jf Gamma t T.[U/]
  intros.Gamma: var -> ty
t: term
T, U: ty
H: jf (Gamma >> ren (+1)) t T
jf Gamma t T.[U/]
  forward jf_jt.Gamma: var -> ty
t: term
T, U: ty
H: jf (Gamma >> ren (+1)) t T
H0: jt (Gamma >> ren (+1)) t T
jf Gamma t T.[U/]
  unfold jt in *.Gamma: var -> ty
t: term
T, U: ty
H: jf (Gamma >> ren (+1)) t T
H0: exists n : nat, jtn n (Gamma >> ren (+1)) t T
jf Gamma t T.[U/] unpack.Gamma: var -> ty
t: term
T, U: ty
H: jf (Gamma >> ren (+1)) t T
x: nat
H0: jtn x (Gamma >> ren (+1)) t T
jf Gamma t T.[U/]
  forward jtn_ty_substitution_0.Gamma: var -> ty
t: term
T, U: ty
H: jf (Gamma >> ren (+1)) t T
x: nat
H0: jtn x (Gamma >> ren (+1)) t T
H1: jtn x Gamma t T.[?Goal/]
jf Gamma t T.[U/]
  eauto using jtn_jf.
Qed.

Renamings of term variables

The typing judgement is preserved by a renaming xi that maps term variables to term variables. Note that xi need not be injective.

Lemma jf_te_renaming:
  forall Gamma t U,
  jf Gamma t U ->
  forall Gamma' xi,
  Gamma = xi >>> Gamma' ->
  jf Gamma' t.[ren xi] U.forall (Gamma : tyenv) (t : term) (U : ty),
jf Gamma t U ->
forall (Gamma' : var -> ty) (xi : var -> var),
Gamma = xi >>> Gamma' -> jf Gamma' t.[ren xi] U
Proof.forall (Gamma : tyenv) (t : term) (U : ty),
jf Gamma t U ->
forall (Gamma' : var -> ty) (xi : var -> var),
Gamma = xi >>> Gamma' -> jf Gamma' t.[ren xi] U
  (* A detailed proof, where every case is dealt with explicitly: *)
  induction 1; intros; subst.x: var
Gamma': var -> ty
xi: var -> var
jf Gamma' (Var x).[ren xi] ((xi >>> Gamma') x)
t: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] U
H: jf (T .: xi >>> Gamma') t U
jf Gamma' (Lam t).[ren xi] (TyFun T U)
t1, t2: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf2: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t2.[ren xi0] T
IHjf1: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t1.[ren xi0] (TyFun T U)
H0: jf (xi >>> Gamma') t2 T
H: jf (xi >>> Gamma') t1 (TyFun T U)
jf Gamma' (App t1 t2).[ren xi] U
t: term
T: ty
Gamma'0: var -> ty
xi: var -> var
IHjf: forall (Gamma' : var -> ty) (xi0 : var -> var),
xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' ->
jf Gamma' t.[ren xi0] T
H: jf (xi >>> Gamma'0 >> ren (+1)) t T
jf Gamma'0 t.[ren xi] (TyAll T)
t: term
T, U: {bind ty}
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] (TyAll T)
H: jf (xi >>> Gamma') t (TyAll T)
jf Gamma' t.[ren xi] T.[U/]
  (* JFVar *)
  {x: var
Gamma': var -> ty
xi: var -> var
jf Gamma' (Var x).[ren xi] ((xi >>> Gamma') x) asimpl.x: var
Gamma': var -> ty
xi: var -> var
jf Gamma' (ids (xi x)) (Gamma' (xi x)) econstructor.x: var
Gamma': var -> ty
xi: var -> var
Gamma' (xi x) = Gamma' (xi x)
      eauto. }t: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] U
H: jf (T .: xi >>> Gamma') t U
jf Gamma' (Lam t).[ren xi] (TyFun T U)
t1, t2: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf2: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t2.[ren xi0] T
IHjf1: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t1.[ren xi0] (TyFun T U)
H0: jf (xi >>> Gamma') t2 T
H: jf (xi >>> Gamma') t1 (TyFun T U)
jf Gamma' (App t1 t2).[ren xi] U
t: term
T: ty
Gamma'0: var -> ty
xi: var -> var
IHjf: forall (Gamma' : var -> ty) (xi0 : var -> var),
xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' ->
jf Gamma' t.[ren xi0] T
H: jf (xi >>> Gamma'0 >> ren (+1)) t T
jf Gamma'0 t.[ren xi] (TyAll T)
t: term
T, U: {bind ty}
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] (TyAll T)
H: jf (xi >>> Gamma') t (TyAll T)
jf Gamma' t.[ren xi] T.[U/]
  (* JFLam *)
  {t: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] U
H: jf (T .: xi >>> Gamma') t U
jf Gamma' (Lam t).[ren xi] (TyFun T U) asimpl.t: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] U
H: jf (T .: xi >>> Gamma') t U
jf Gamma' (Lam t.[ren (upren xi)]) (TyFun T U) econstructor.t: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] U
H: jf (T .: xi >>> Gamma') t U
jf (T .: Gamma') t.[ren (upren xi)] U
      eapply IHjf.t: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
T .: xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] U
H: jf (T .: xi >>> Gamma') t U
T .: xi >>> Gamma' = upren xi >>> T .: Gamma' autosubst. }t1, t2: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf2: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t2.[ren xi0] T
IHjf1: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t1.[ren xi0] (TyFun T U)
H0: jf (xi >>> Gamma') t2 T
H: jf (xi >>> Gamma') t1 (TyFun T U)
jf Gamma' (App t1 t2).[ren xi] U
t: term
T: ty
Gamma'0: var -> ty
xi: var -> var
IHjf: forall (Gamma' : var -> ty) (xi0 : var -> var),
xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' ->
jf Gamma' t.[ren xi0] T
H: jf (xi >>> Gamma'0 >> ren (+1)) t T
jf Gamma'0 t.[ren xi] (TyAll T)
t: term
T, U: {bind ty}
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] (TyAll T)
H: jf (xi >>> Gamma') t (TyAll T)
jf Gamma' t.[ren xi] T.[U/]
  (* JFApp *)
  {t1, t2: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf2: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t2.[ren xi0] T
IHjf1: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t1.[ren xi0] (TyFun T U)
H0: jf (xi >>> Gamma') t2 T
H: jf (xi >>> Gamma') t1 (TyFun T U)
jf Gamma' (App t1 t2).[ren xi] U asimpl.t1, t2: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf2: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t2.[ren xi0] T
IHjf1: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t1.[ren xi0] (TyFun T U)
H0: jf (xi >>> Gamma') t2 T
H: jf (xi >>> Gamma') t1 (TyFun T U)
jf Gamma' (App t1.[ren xi] t2.[ren xi]) U econstructor.t1, t2: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf2: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t2.[ren xi0] T
IHjf1: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t1.[ren xi0] (TyFun T U)
H0: jf (xi >>> Gamma') t2 T
H: jf (xi >>> Gamma') t1 (TyFun T U)
jf Gamma' t1.[ren xi] (TyFun ?T U)
t1, t2: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf2: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t2.[ren xi0] T
IHjf1: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t1.[ren xi0] (TyFun T U)
H0: jf (xi >>> Gamma') t2 T
H: jf (xi >>> Gamma') t1 (TyFun T U)
jf Gamma' t2.[ren xi] ?T
      eauto.t1, t2: term
T, U: ty
Gamma': var -> ty
xi: var -> var
IHjf2: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t2.[ren xi0] T
IHjf1: forall (Gamma'0 : var -> ty)
  (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t1.[ren xi0] (TyFun T U)
H0: jf (xi >>> Gamma') t2 T
H: jf (xi >>> Gamma') t1 (TyFun T U)
jf Gamma' t2.[ren xi] T
      eauto. }t: term
T: ty
Gamma'0: var -> ty
xi: var -> var
IHjf: forall (Gamma' : var -> ty) (xi0 : var -> var),
xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' ->
jf Gamma' t.[ren xi0] T
H: jf (xi >>> Gamma'0 >> ren (+1)) t T
jf Gamma'0 t.[ren xi] (TyAll T)
t: term
T, U: {bind ty}
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] (TyAll T)
H: jf (xi >>> Gamma') t (TyAll T)
jf Gamma' t.[ren xi] T.[U/]
  (* JFTyAbs *)
  {t: term
T: ty
Gamma'0: var -> ty
xi: var -> var
IHjf: forall (Gamma' : var -> ty) (xi0 : var -> var),
xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' ->
jf Gamma' t.[ren xi0] T
H: jf (xi >>> Gamma'0 >> ren (+1)) t T
jf Gamma'0 t.[ren xi] (TyAll T) asimpl.t: term
T: ty
Gamma'0: var -> ty
xi: var -> var
IHjf: forall (Gamma' : var -> ty) (xi0 : var -> var),
xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' ->
jf Gamma' t.[ren xi0] T
H: jf (xi >>> Gamma'0 >> ren (+1)) t T
jf Gamma'0 t.[ren xi] (TyAll T) econstructor.t: term
T: ty
Gamma'0: var -> ty
xi: var -> var
IHjf: forall (Gamma' : var -> ty) (xi0 : var -> var),
xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' ->
jf Gamma' t.[ren xi0] T
H: jf (xi >>> Gamma'0 >> ren (+1)) t T
jf ?Gamma' t.[ren xi] T
t: term
T: ty
Gamma'0: var -> ty
xi: var -> var
IHjf: forall (Gamma' : var -> ty) (xi0 : var -> var),
xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' ->
jf Gamma' t.[ren xi0] T
H: jf (xi >>> Gamma'0 >> ren (+1)) t T
?Gamma' = Gamma'0 >> ren (+1)
      eapply IHjf.t: term
T: ty
Gamma'0: var -> ty
xi: var -> var
IHjf: forall (Gamma' : var -> ty) (xi0 : var -> var),
xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' ->
jf Gamma' t.[ren xi0] T
H: jf (xi >>> Gamma'0 >> ren (+1)) t T
xi >>> Gamma'0 >> ren (+1) = xi >>> ?Gamma'
t: term
T: ty
Gamma'0: var -> ty
xi: var -> var
IHjf: forall (Gamma' : var -> ty) (xi0 : var -> var),
xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' ->
jf Gamma' t.[ren xi0] T
H: jf (xi >>> Gamma'0 >> ren (+1)) t T
?Gamma' = Gamma'0 >> ren (+1) autosubst.t: term
T: ty
Gamma'0: var -> ty
xi: var -> var
IHjf: forall (Gamma' : var -> ty) (xi0 : var -> var),
xi >>> Gamma'0 >> ren (+1) = xi0 >>> Gamma' ->
jf Gamma' t.[ren xi0] T
H: jf (xi >>> Gamma'0 >> ren (+1)) t T
Gamma'0 >>> subst ((+1) >>> ids) = Gamma'0 >> ren (+1)
      autosubst. }t: term
T, U: {bind ty}
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] (TyAll T)
H: jf (xi >>> Gamma') t (TyAll T)
jf Gamma' t.[ren xi] T.[U/]
  (* JFTyApp *)
  {t: term
T, U: {bind ty}
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] (TyAll T)
H: jf (xi >>> Gamma') t (TyAll T)
jf Gamma' t.[ren xi] T.[U/] asimpl.t: term
T, U: {bind ty}
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] (TyAll T)
H: jf (xi >>> Gamma') t (TyAll T)
jf Gamma' t.[ren xi] T.[U/] econstructor.t: term
T, U: {bind ty}
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] (TyAll T)
H: jf (xi >>> Gamma') t (TyAll T)
jf Gamma' t.[ren xi] (TyAll ?T)
t: term
T, U: {bind ty}
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] (TyAll T)
H: jf (xi >>> Gamma') t (TyAll T)
T.[U/] = ?T.[?U/]
      eauto.t: term
T, U: {bind ty}
Gamma': var -> ty
xi: var -> var
IHjf: forall (Gamma'0 : var -> ty) (xi0 : var -> var),
xi >>> Gamma' = xi0 >>> Gamma'0 ->
jf Gamma'0 t.[ren xi0] (TyAll T)
H: jf (xi >>> Gamma') t (TyAll T)
T.[U/] = T.[?U/]
      eauto. }
Restart.forall (Gamma : tyenv) (t : term) (U : ty),
jf Gamma t U ->
forall (Gamma' : var -> ty) (xi : var -> var),
Gamma = xi >>> Gamma' -> jf Gamma' t.[ren xi] U
  (* A shorter script, where all cases are dealt with uniformly: *)
  induction 1; intros; subst;
  asimpl; econstructor; eauto with autosubst.
Qed.

As a corollary, jf is preserved by the renaming (+1).

Lemma jf_te_renaming_0:
  forall Gamma t T U,
  jf Gamma t U ->
  jf (T .: Gamma) (lift 1 t) U.forall (Gamma : tyenv) (t : term) (T U : ty),
jf Gamma t U -> jf (T .: Gamma) (lift 1 t) U
Proof.forall (Gamma : tyenv) (t : term) (T U : ty),
jf Gamma t U -> jf (T .: Gamma) (lift 1 t) U
  intros.Gamma: tyenv
t: term
T, U: ty
H: jf Gamma t U
jf (T .: Gamma) (lift 1 t) U eapply jf_te_renaming.Gamma: tyenv
t: term
T, U: ty
H: jf Gamma t U
jf ?Gamma t U
Gamma: tyenv
t: term
T, U: ty
H: jf Gamma t U
?Gamma = (+1) >>> T .: Gamma eauto.Gamma: tyenv
t: term
T, U: ty
H: jf Gamma t U
Gamma = (+1) >>> T .: Gamma autosubst.
Qed.

Substitutions of terms for term variables

The typing judgement is extended to substitutions.

Definition js Gamma sigma Delta :=
  forall x : var,
  jf Gamma (sigma x) (Delta x).

The following are basic lemmas about js.

Lemma js_ids:
  forall Gamma,
  js Gamma ids Gamma.forall Gamma : tyenv, js Gamma ids Gamma
Proof.forall Gamma : tyenv, js Gamma ids Gamma
  unfold js.forall (Gamma : tyenv) (x : var),
jf Gamma (ids x) (Gamma x) eauto with jf.
Qed.

Lemma js_cons:
  forall Gamma t sigma T Delta,
  jf Gamma t T ->
  js Gamma sigma Delta ->
  js Gamma (t .: sigma) (T .: Delta).forall (Gamma : tyenv) (t : term)
  (sigma : var -> term) (T : ty) (Delta : var -> ty),
jf Gamma t T ->
js Gamma sigma Delta ->
js Gamma (t .: sigma) (T .: Delta)
Proof.forall (Gamma : tyenv) (t : term)
  (sigma : var -> term) (T : ty) (Delta : var -> ty),
jf Gamma t T ->
js Gamma sigma Delta ->
js Gamma (t .: sigma) (T .: Delta)
  intros.Gamma: tyenv
t: term
sigma: var -> term
T: ty
Delta: var -> ty
H: jf Gamma t T
H0: js Gamma sigma Delta
js Gamma (t .: sigma) (T .: Delta) intros [|x]; asimpl; eauto.
Qed.

Lemma js_up:
  forall Gamma sigma Delta T,
  js Gamma sigma Delta ->
  js (T .: Gamma) (up sigma) (T .: Delta).forall (Gamma : tyenv) (sigma : var -> term)
  (Delta : var -> ty) (T : ty),
js Gamma sigma Delta ->
js (T .: Gamma) (up sigma) (T .: Delta)
Proof.forall (Gamma : tyenv) (sigma : var -> term)
  (Delta : var -> ty) (T : ty),
js Gamma sigma Delta ->
js (T .: Gamma) (up sigma) (T .: Delta)
  intros.Gamma: tyenv
sigma: var -> term
Delta: var -> ty
T: ty
H: js Gamma sigma Delta
js (T .: Gamma) (up sigma) (T .: Delta) intros [|x]; asimpl.Gamma: tyenv
sigma: var -> term
Delta: var -> ty
T: ty
H: js Gamma sigma Delta
jf (T .: Gamma) (ids 0) T
Gamma: tyenv
sigma: var -> term
Delta: var -> ty
T: ty
H: js Gamma sigma Delta
x: nat
jf (T .: Gamma) (lift 1 (sigma x)) (Delta x)
  {Gamma: tyenv
sigma: var -> term
Delta: var -> ty
T: ty
H: js Gamma sigma Delta
jf (T .: Gamma) (ids 0) T eauto with jf. }Gamma: tyenv
sigma: var -> term
Delta: var -> ty
T: ty
H: js Gamma sigma Delta
x: nat
jf (T .: Gamma) (lift 1 (sigma x)) (Delta x)
  {Gamma: tyenv
sigma: var -> term
Delta: var -> ty
T: ty
H: js Gamma sigma Delta
x: nat
jf (T .: Gamma) (lift 1 (sigma x)) (Delta x) eauto using jf_te_renaming_0. }
Qed.

In the following statement, theta is a substitution of types for type variables. It is post-composed with the type environments Gamma and Delta.

Lemma js_ty_substitution:
  forall Gamma sigma Delta theta,
  js Gamma sigma Delta ->
  js (Gamma >> theta) sigma (Delta >> theta).forall (Gamma : tyenv) (sigma : var -> term)
  (Delta theta : var -> ty),
js Gamma sigma Delta ->
js (Gamma >> theta) sigma (Delta >> theta)
Proof.forall (Gamma : tyenv) (sigma : var -> term)
  (Delta theta : var -> ty),
js Gamma sigma Delta ->
js (Gamma >> theta) sigma (Delta >> theta)
  unfold js.forall (Gamma : tyenv) (sigma : var -> term)
  (Delta theta : var -> ty),
(forall x : var, jf Gamma (sigma x) (Delta x)) ->
forall x : var,
jf (Gamma >> theta) (sigma x) ((Delta >> theta) x) eauto using jf_ty_substitution.
Qed.

The typing judgement is preserved by a well-typed substitution sigma of (all) term variables to terms.

Lemma jf_te_substitution:
  forall Delta t U,
  jf Delta t U ->
  forall Gamma sigma,
  js Gamma sigma Delta ->
  jf Gamma t.[sigma] U.forall (Delta : tyenv) (t : term) (U : ty),
jf Delta t U ->
forall (Gamma : tyenv) (sigma : var -> term),
js Gamma sigma Delta -> jf Gamma t.[sigma] U
Proof.forall (Delta : tyenv) (t : term) (U : ty),
jf Delta t U ->
forall (Gamma : tyenv) (sigma : var -> term),
js Gamma sigma Delta -> jf Gamma t.[sigma] U
  induction 1; intros; subst; asimpl;
  eauto using js_up, js_ty_substitution with jf.
Qed.

As a corollary, the typing judgement is preserved by a well-typed substitution of one term for one variable, namely variable 0.

This property is exploited in the proof of subject reduction, in the case of beta-reduction.

Lemma jf_te_substitution_0:
  forall Gamma t1 t2 T U,
  jf (T .: Gamma) t1 U ->
  jf Gamma t2 T ->
  jf Gamma t1.[t2/] U.forall (Gamma : var -> ty) (t1 t2 : term) (T U : ty),
jf (T .: Gamma) t1 U ->
jf Gamma t2 T -> jf Gamma t1.[t2/] U
Proof.forall (Gamma : var -> ty) (t1 t2 : term) (T U : ty),
jf (T .: Gamma) t1 U ->
jf Gamma t2 T -> jf Gamma t1.[t2/] U
  eauto using jf_te_substitution, js_ids, js_cons.
Qed.