Contexts.v

From Tealeaves Require Import
  Functors.List
  Backends.Multisorted.LN
  Examples.SystemF.Syntax
  Simplification.Tests.SystemF_LN.

From Coq Require Import
  Sorting.Permutation.

Implicit Types (x : atom).

Import AtomSet.Notations.
Import ContainerFunctor.Notations.
Import AssocList.Notations.
Import List.ListNotations.

Create HintDb sysf_ctx.

#[local] Generalizable Variables F G A B C ϕ W T.
#[local] Open Scope set_scope.

(* Misc *)

Lemma rw_subst_type_var_neq {x y} τ':
  x <> y ->
  subst typ ktyp x τ' (ty_v (Fr y)) = ty_v (Fr y).x, y: atom
τ': SystemF ktyp LN
x <> y ->
subst typ ktyp x τ' (ty_v (Fr y)) = ty_v (Fr y)
Proof.x, y: atom
τ': SystemF ktyp LN
x <> y ->
subst typ ktyp x τ' (ty_v (Fr y)) = ty_v (Fr y)
  intros.x, y: atom
τ': SystemF ktyp LN
H: x <> y
subst typ ktyp x τ' (ty_v (Fr y)) = ty_v (Fr y)
  simplify_subst.x, y: atom
τ': SystemF ktyp LN
H: x <> y
btg ktyp (subst_loc ktyp x τ') ktyp (Fr y) =
ty_v (Fr y)
  cbn.x, y: atom
τ': SystemF ktyp LN
H: x <> y
(if x == y then τ' else ty_v (Fr y)) = ty_v (Fr y) destruct_eq_args x y.
Qed.

Lemma rw_subst_term_var_neq {x y} {τ} :
  x <> y ->
  subst term ktyp x τ (tm_var (Fr y)) = tm_var (Fr y).x, y: atom
τ: SystemF ktyp LN
x <> y ->
subst term ktyp x τ (tm_var (Fr y)) = tm_var (Fr y)
Proof.x, y: atom
τ: SystemF ktyp LN
x <> y ->
subst term ktyp x τ (tm_var (Fr y)) = tm_var (Fr y)
  intros.x, y: atom
τ: SystemF ktyp LN
H: x <> y
subst term ktyp x τ (tm_var (Fr y)) = tm_var (Fr y)
  simplify_subst.x, y: atom
τ: SystemF ktyp LN
H: x <> y
btg ktyp (subst_loc ktyp x τ) ktrm (Fr y) =
tm_var (Fr y)
  cbn.x, y: atom
τ: SystemF ktyp LN
H: x <> y
tm_var (Fr y) = tm_var (Fr y) destruct_eq_args x y.
Qed.

Lemma FV_trm_type_empty: forall τ,
    FV typ ktrm τ [=] ∅.forall τ : typ LN, FV typ ktrm τ [=] ∅
Proof.forall τ : typ LN, FV typ ktrm τ [=] ∅
  intros.τ: typ LN
FV typ ktrm τ [=] ∅
  induction τ; simplify_FV; fsetdec.
Qed.

Lemma subst_in_type_id: forall x u τ,
    subst typ ktrm x u τ = τ.forall x (u : SystemF ktrm LN) (τ : typ LN),
subst typ ktrm x u τ = τ
Proof.forall x (u : SystemF ktrm LN) (τ : typ LN),
subst typ ktrm x u τ = τ
  intros.x: atom
u: SystemF ktrm LN
τ: typ LN
subst typ ktrm x u τ = τ
  eapply (subst_fresh_set typ).x: atom
u: SystemF ktrm LN
τ: typ LN
x `notin` FV typ ktrm τ
  rewrite FV_trm_type_empty.x: atom
u: SystemF ktrm LN
τ: typ LN
x `notin` ∅
  fsetdec.
Qed.

Lemma LC_typ_trm: forall τ,
    LC typ ktrm τ.forall τ : typ LN, LC typ ktrm τ
Proof.forall τ : typ LN, LC typ ktrm τ
  intros.τ: typ LN
LC typ ktrm τ induction τ; now simplify_LC.
Qed.

(** * Tactical support *)
(******************************************************************************)
Ltac burst :=
  rewrite_strat
    outermost
    (choice (hints tea_rw_dom)
            (choice (hints tea_rw_range)
                    (choice (hints tea_rw_disj)
                            (choice (hints tea_rw_uniq)
                                    (hints tea_list))))).

Tactic Notation "burst" "in" hyp(H) :=
  rewrite_strat
    outermost
    (choice (hints tea_rw_dom)
            (choice (hints tea_rw_range)
                    (choice (hints tea_rw_disj)
                            (choice (hints tea_rw_uniq)
                                    (hints tea_list))))) in H.

Tactic Notation "bursts" :=
  repeat match goal with
         | H : _ |- _ => burst in H
         end; repeat burst.

(** * Structural lemmas for <<scoped>> *)
(** These lemmas are actually independent of System F. They could be
    incorporated into the locally nameless backend. *)
(******************************************************************************)
Section scope_lemmas.

  Context
    (S : Type -> Type)
    `{MultiDecoratedTraversablePreModule (list K) T S (mn_op := Monoid_op_list) (mn_unit := Monoid_unit_list)}
    `{! MultiDecoratedTraversableMonad (list K) T}.

  (** *** Permutation *)
  (******************************************************************************)
  Lemma scoped_perm : forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
      Permutation γ1 γ2 ->
      scoped S k t (domset γ1) ->
      scoped S k t (domset γ2).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
Permutation γ1 γ2 ->
scoped S k t (domset γ1) -> scoped S k t (domset γ2)
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
Permutation γ1 γ2 ->
scoped S k t (domset γ1) -> scoped S k t (domset γ2)
    introv Hperm.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
Hperm: Permutation γ1 γ2
scoped S k t (domset γ1) -> scoped S k t (domset γ2) unfold scoped.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
Hperm: Permutation γ1 γ2
FV S k t ⊆ domset γ1 -> FV S k t ⊆ domset γ2 rewrite (perm_domset); eauto.
  Qed.

  Theorem scoped_perm_iff : forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
      Permutation γ1 γ2 ->
      scoped S k t (domset γ1) <->
      scoped S k t (domset γ2).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
Permutation γ1 γ2 ->
scoped S k t (domset γ1) <-> scoped S k t (domset γ2)
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
Permutation γ1 γ2 ->
scoped S k t (domset γ1) <-> scoped S k t (domset γ2)
    intros.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
H1: Permutation γ1 γ2
scoped S k t (domset γ1) <-> scoped S k t (domset γ2) assert (Permutation γ2 γ1) by now symmetry.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
H1: Permutation γ1 γ2
H2: Permutation γ2 γ1
scoped S k t (domset γ1) <-> scoped S k t (domset γ2)
    split; eauto using scoped_perm.
  Qed.

  Corollary scoped_perm_comm : forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
      scoped S k t (domset (γ1 ++ γ2)) <->
      scoped S k t (domset (γ2 ++ γ1)).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
scoped S k t (domset (γ1 ++ γ2)) <->
scoped S k t (domset (γ2 ++ γ1))
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
scoped S k t (domset (γ1 ++ γ2)) <->
scoped S k t (domset (γ2 ++ γ1))
    intros.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
scoped S k t (domset (γ1 ++ γ2)) <->
scoped S k t (domset (γ2 ++ γ1)) apply scoped_perm_iff.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
Permutation (γ1 ++ γ2) (γ2 ++ γ1) apply Permutation_app_comm.
  Qed.

  (** *** Weakening *)
  (******************************************************************************)
  Lemma scoped_weak_l : forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
      scoped S k t (domset γ1) ->
      scoped S k t (domset (γ1 ++ γ2)).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
scoped S k t (domset γ1) ->
scoped S k t (domset (γ1 ++ γ2))
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
scoped S k t (domset γ1) ->
scoped S k t (domset (γ1 ++ γ2))
    intros.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
H1: scoped S k t (domset γ1)
scoped S k t (domset (γ1 ++ γ2)) unfold scoped in *.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
H1: FV S k t ⊆ domset γ1
FV S k t ⊆ domset (γ1 ++ γ2)
    autorewrite with tea_rw_dom.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
H1: FV S k t ⊆ domset γ1
FV S k t ⊆ domset γ1 ∪ domset γ2 fsetdec.
  Qed.

  Lemma scoped_weak_mid : forall (k : K) (t : S LN) (X : Type) (γ1 γ2 γ : alist X),
      scoped S k t (domset (γ1 ++ γ2)) ->
      scoped S k t (domset (γ1 ++ γ ++ γ2)).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type)
  (γ1 γ2 γ : alist X),
scoped S k t (domset (γ1 ++ γ2)) ->
scoped S k t (domset (γ1 ++ γ ++ γ2))
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type)
  (γ1 γ2 γ : alist X),
scoped S k t (domset (γ1 ++ γ2)) ->
scoped S k t (domset (γ1 ++ γ ++ γ2))
    intros.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2, γ: alist X
H1: scoped S k t (domset (γ1 ++ γ2))
scoped S k t (domset (γ1 ++ γ ++ γ2)) unfold scoped in *.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2, γ: alist X
H1: FV S k t ⊆ domset (γ1 ++ γ2)
FV S k t ⊆ domset (γ1 ++ γ ++ γ2)
    autorewrite with tea_rw_dom in *.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2, γ: alist X
H1: FV S k t ⊆ domset γ1 ∪ domset γ2
FV S k t ⊆ domset γ1 ∪ (domset γ ∪ domset γ2) fsetdec.
  Qed.

  Lemma scoped_weak_r : forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
      scoped S k t (domset γ2) ->
      scoped S k t (domset (γ1 ++ γ2)).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
scoped S k t (domset γ2) ->
scoped S k t (domset (γ1 ++ γ2))
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X),
scoped S k t (domset γ2) ->
scoped S k t (domset (γ1 ++ γ2))
    intros.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
H1: scoped S k t (domset γ2)
scoped S k t (domset (γ1 ++ γ2)) unfold scoped in *.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
H1: FV S k t ⊆ domset γ2
FV S k t ⊆ domset (γ1 ++ γ2)
    autorewrite with tea_rw_dom.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
H1: FV S k t ⊆ domset γ2
FV S k t ⊆ domset γ1 ∪ domset γ2 fsetdec.
  Qed.

  (** *** Strengthening *)
  (******************************************************************************)
  Lemma scoped_stren_mid : forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X) (x : atom) (x' : X),
      scoped S k t (domset (γ1 ++ x ~ x' ++ γ2)) ->
      ~ x `in` (FV S k t) ->
      scoped S k t (domset (γ1 ++ γ2)).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X)
  x (x' : X),
scoped S k t (domset (γ1 ++ x ~ x' ++ γ2)) ->
x `notin` FV S k t -> scoped S k t (domset (γ1 ++ γ2))
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ1 γ2 : alist X)
  x (x' : X),
scoped S k t (domset (γ1 ++ x ~ x' ++ γ2)) ->
x `notin` FV S k t -> scoped S k t (domset (γ1 ++ γ2))
    introv hyp hnotin.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
x: atom
x': X
hyp: scoped S k t (domset (γ1 ++ x ~ x' ++ γ2))
hnotin: x `notin` FV S k t
scoped S k t (domset (γ1 ++ γ2)) unfold scoped in *.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
x: atom
x': X
hyp: FV S k t ⊆ domset (γ1 ++ x ~ x' ++ γ2)
hnotin: x `notin` FV S k t
FV S k t ⊆ domset (γ1 ++ γ2)
    autorewrite with tea_rw_dom in *.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ1, γ2: alist X
x: atom
x': X
hyp: FV S k t ⊆ domset γ1 ∪ ({{x}} ∪ domset γ2)
hnotin: x `notin` FV S k t
FV S k t ⊆ domset γ1 ∪ domset γ2 fsetdec.
  Qed.

  Corollary scoped_stren_l : forall (k : K) (t : S LN) (X : Type) (γ : alist X) (x : atom) (x' : X),
      scoped S k t (domset (x ~ x' ++ γ)) ->
      ~ x `in` (FV S k t) ->
      scoped S k t (domset γ).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ : alist X) 
  x (x' : X),
scoped S k t (domset (x ~ x' ++ γ)) ->
x `notin` FV S k t -> scoped S k t (domset γ)
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ : alist X) 
  x (x' : X),
scoped S k t (domset (x ~ x' ++ γ)) ->
x `notin` FV S k t -> scoped S k t (domset γ)
    introv Hscope Hnotin.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ: alist X
x: atom
x': X
Hscope: scoped S k t (domset (x ~ x' ++ γ))
Hnotin: x `notin` FV S k t
scoped S k t (domset γ) change γ with (nil ++ γ).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ: alist X
x: atom
x': X
Hscope: scoped S k t (domset (x ~ x' ++ γ))
Hnotin: x `notin` FV S k t
scoped S k t (domset ([] ++ γ))
    eapply scoped_stren_mid; [apply Hscope | apply Hnotin].
  Qed.

  Corollary scoped_stren_r : forall (k : K) (t : S LN) (X : Type) (γ : alist X) (x : atom) (x' : X),
      scoped S k t (domset (γ ++ x ~ x')) ->
      ~ x `in` (FV S k t) ->
      scoped S k t (domset γ).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ : alist X) 
  x (x' : X),
scoped S k t (domset (γ ++ x ~ x')) ->
x `notin` FV S k t -> scoped S k t (domset γ)
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t : S LN) (X : Type) (γ : alist X) 
  x (x' : X),
scoped S k t (domset (γ ++ x ~ x')) ->
x `notin` FV S k t -> scoped S k t (domset γ)
    introv Hscope Hnotin.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ: alist X
x: atom
x': X
Hscope: scoped S k t (domset (γ ++ x ~ x'))
Hnotin: x `notin` FV S k t
scoped S k t (domset γ) replace γ with (γ ++ nil) by (now List.simpl_list).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t: S LN
X: Type
γ: alist X
x: atom
x': X
Hscope: scoped S k t (domset (γ ++ x ~ x'))
Hnotin: x `notin` FV S k t
scoped S k t (domset (γ ++ []))
    eapply scoped_stren_mid; [apply Hscope | apply Hnotin].
  Qed.

  (** *** Substitution *)
  (******************************************************************************)
  Lemma scoped_sub_eq_mid :
    forall (k : K) (t1 : S LN) (t2 : T k LN)
      (X : Type) (γ1 γ2 : alist X) (x : atom) (x' : X),
      scoped S k t1 (domset (γ1 ++ x ~ x' ++ γ2)) ->
      scoped (T k) k t2 (domset (γ1 ++ γ2)) ->
      scoped S k (subst S k x t2 t1) (domset (γ1 ++ γ2)).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t1 : S LN) (t2 : T k LN) (X : Type)
  (γ1 γ2 : alist X) x (x' : X),
scoped S k t1 (domset (γ1 ++ x ~ x' ++ γ2)) ->
scoped (T k) k t2 (domset (γ1 ++ γ2)) ->
scoped S k (subst S k x t2 t1) (domset (γ1 ++ γ2))
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t1 : S LN) (t2 : T k LN) (X : Type)
  (γ1 γ2 : alist X) x (x' : X),
scoped S k t1 (domset (γ1 ++ x ~ x' ++ γ2)) ->
scoped (T k) k t2 (domset (γ1 ++ γ2)) ->
scoped S k (subst S k x t2 t1) (domset (γ1 ++ γ2))
    introv hyp1 hyp2.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1, γ2: alist X
x: atom
x': X
hyp1: scoped S k t1 (domset (γ1 ++ x ~ x' ++ γ2))
hyp2: scoped (T k) k t2 (domset (γ1 ++ γ2))
scoped S k (subst S k x t2 t1) (domset (γ1 ++ γ2)) unfold scoped in *.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1, γ2: alist X
x: atom
x': X
hyp1: FV S k t1 ⊆ domset (γ1 ++ x ~ x' ++ γ2)
hyp2: FV (T k) k t2 ⊆ domset (γ1 ++ γ2)
FV S k (subst S k x t2 t1) ⊆ domset (γ1 ++ γ2) autorewrite with tea_rw_dom in *.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1, γ2: alist X
x: atom
x': X
hyp1: FV S k t1 ⊆ domset γ1 ∪ ({{x}} ∪ domset γ2)
hyp2: FV (T k) k t2 ⊆ domset γ1 ∪ domset γ2
FV S k (subst S k x t2 t1) ⊆ domset γ1 ∪ domset γ2
    etransitivity.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1, γ2: alist X
x: atom
x': X
hyp1: FV S k t1 ⊆ domset γ1 ∪ ({{x}} ∪ domset γ2)
hyp2: FV (T k) k t2 ⊆ domset γ1 ∪ domset γ2
FV S k (subst S k x t2 t1) ⊆ ?y
S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1, γ2: alist X
x: atom
x': X
hyp1: FV S k t1 ⊆ domset γ1 ∪ ({{x}} ∪ domset γ2)
hyp2: FV (T k) k t2 ⊆ domset γ1 ∪ domset γ2
?y ⊆ domset γ1 ∪ domset γ2 apply (FV_subst_upper_eq S).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1, γ2: alist X
x: atom
x': X
hyp1: FV S k t1 ⊆ domset γ1 ∪ ({{x}} ∪ domset γ2)
hyp2: FV (T k) k t2 ⊆ domset γ1 ∪ domset γ2
FV S k t1 \\ {{x}} ∪ FV (T k) k t2
⊆ domset γ1 ∪ domset γ2 fsetdec.
  Qed.

  Corollary scoped_sub_eq_r :
    forall (k : K) (t1 : S LN) (t2 : T k LN)
      (X : Type) (γ1 : alist X) (x : atom) (x' : X),
      scoped S k t1 (domset (γ1 ++ x ~ x')) ->
      scoped (T k) k t2 (domset γ1) ->
      scoped S k (subst S k x t2 t1) (domset γ1).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t1 : S LN) (t2 : T k LN) (X : Type)
  (γ1 : alist X) x (x' : X),
scoped S k t1 (domset (γ1 ++ x ~ x')) ->
scoped (T k) k t2 (domset γ1) ->
scoped S k (subst S k x t2 t1) (domset γ1)
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t1 : S LN) (t2 : T k LN) (X : Type)
  (γ1 : alist X) x (x' : X),
scoped S k t1 (domset (γ1 ++ x ~ x')) ->
scoped (T k) k t2 (domset γ1) ->
scoped S k (subst S k x t2 t1) (domset γ1)
    introv hyp1 hyp2.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1: alist X
x: atom
x': X
hyp1: scoped S k t1 (domset (γ1 ++ x ~ x'))
hyp2: scoped (T k) k t2 (domset γ1)
scoped S k (subst S k x t2 t1) (domset γ1) change_alist (γ1 ++ x ~ x' ++ []) in hyp1.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1: alist X
x: atom
x': X
hyp1: scoped S k t1 (domset (γ1 ++ x ~ x' ++ []))
hyp2: scoped (T k) k t2 (domset γ1)
scoped S k (subst S k x t2 t1) (domset γ1)
    change_alist (γ1 ++ []) in hyp2.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1: alist X
x: atom
x': X
hyp1: scoped S k t1 (domset (γ1 ++ x ~ x' ++ []))
hyp2: scoped (T k) k t2 (domset (γ1 ++ []))
scoped S k (subst S k x t2 t1) (domset γ1)
    change_alist (γ1 ++ []).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1: alist X
x: atom
x': X
hyp1: scoped S k t1 (domset (γ1 ++ x ~ x' ++ []))
hyp2: scoped (T k) k t2 (domset (γ1 ++ []))
scoped S k (subst S k x t2 t1) (domset (γ1 ++ []))
    eapply scoped_sub_eq_mid; eauto.
  Qed.

  Corollary scoped_sub_eq_l :
    forall (k : K) (t1 : S LN) (t2 : T k LN)
      (X : Type) (γ1 : alist X) (x : atom) (x' : X),
      scoped S k t1 (domset (x ~ x' ++ γ1)) ->
      scoped (T k) k t2 (domset γ1) ->
      scoped S k (subst S k x t2 t1) (domset γ1).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t1 : S LN) (t2 : T k LN) (X : Type)
  (γ1 : alist X) x (x' : X),
scoped S k t1 (domset (x ~ x' ++ γ1)) ->
scoped (T k) k t2 (domset γ1) ->
scoped S k (subst S k x t2 t1) (domset γ1)
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t1 : S LN) (t2 : T k LN) (X : Type)
  (γ1 : alist X) x (x' : X),
scoped S k t1 (domset (x ~ x' ++ γ1)) ->
scoped (T k) k t2 (domset γ1) ->
scoped S k (subst S k x t2 t1) (domset γ1)
    introv hyp1 hyp2.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1: alist X
x: atom
x': X
hyp1: scoped S k t1 (domset (x ~ x' ++ γ1))
hyp2: scoped (T k) k t2 (domset γ1)
scoped S k (subst S k x t2 t1) (domset γ1) change_alist ([] ++ x ~ x' ++ γ1) in hyp1.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1: alist X
x: atom
x': X
hyp1: scoped S k t1 (domset ([] ++ x ~ x' ++ γ1))
hyp2: scoped (T k) k t2 (domset γ1)
scoped S k (subst S k x t2 t1) (domset γ1)
    change_alist ([] ++ γ1) in hyp2.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1: alist X
x: atom
x': X
hyp1: scoped S k t1 (domset ([] ++ x ~ x' ++ γ1))
hyp2: scoped (T k) k t2 (domset ([] ++ γ1))
scoped S k (subst S k x t2 t1) (domset γ1)
    change_alist ([] ++ γ1).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
t2: T k LN
X: Type
γ1: alist X
x: atom
x': X
hyp1: scoped S k t1 (domset ([] ++ x ~ x' ++ γ1))
hyp2: scoped (T k) k t2 (domset ([] ++ γ1))
scoped S k (subst S k x t2 t1) (domset ([] ++ γ1))
    eapply scoped_sub_eq_mid; eauto.
  Qed.

  Lemma scoped_sub_neq :
    forall (k1 k2 : K) (neq : k1 <> k2) (t1 : S LN) (t2 : T k2 LN)
      (X : Type) (γ : alist X) (x : atom),
      scoped S k1 t1 (domset γ) ->
      scoped (T k2) k1 t2 (domset γ) ->
      scoped S k1 (subst S k2 x t2 t1) (domset γ).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall k1 k2 : K,
k1 <> k2 ->
forall (t1 : S LN) (t2 : T k2 LN) (X : Type)
  (γ : alist X) x,
scoped S k1 t1 (domset γ) ->
scoped (T k2) k1 t2 (domset γ) ->
scoped S k1 (subst S k2 x t2 t1) (domset γ)
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall k1 k2 : K,
k1 <> k2 ->
forall (t1 : S LN) (t2 : T k2 LN) (X : Type)
  (γ : alist X) x,
scoped S k1 t1 (domset γ) ->
scoped (T k2) k1 t2 (domset γ) ->
scoped S k1 (subst S k2 x t2 t1) (domset γ)
    introv hyp1 hyp2.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k1, k2: K
hyp1: k1 <> k2
t1: S LN
t2: T k2 LN
X: Type
γ: alist X
x: atom
hyp2: scoped S k1 t1 (domset γ)
scoped (T k2) k1 t2 (domset γ) ->
scoped S k1 (subst S k2 x t2 t1) (domset γ) unfold scoped in *.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k1, k2: K
hyp1: k1 <> k2
t1: S LN
t2: T k2 LN
X: Type
γ: alist X
x: atom
hyp2: FV S k1 t1 ⊆ domset γ
FV (T k2) k1 t2 ⊆ domset γ ->
FV S k1 (subst S k2 x t2 t1) ⊆ domset γ autorewrite with tea_rw_dom in *.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k1, k2: K
hyp1: k1 <> k2
t1: S LN
t2: T k2 LN
X: Type
γ: alist X
x: atom
hyp2: FV S k1 t1 ⊆ domset γ
FV (T k2) k1 t2 ⊆ domset γ ->
FV S k1 (subst S k2 x t2 t1) ⊆ domset γ
    etransitivity.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k1, k2: K
hyp1: k1 <> k2
t1: S LN
t2: T k2 LN
X: Type
γ: alist X
x: atom
hyp2: FV S k1 t1 ⊆ domset γ
H1: FV (T k2) k1 t2 ⊆ domset γ
FV S k1 (subst S k2 x t2 t1) ⊆ ?y
S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k1, k2: K
hyp1: k1 <> k2
t1: S LN
t2: T k2 LN
X: Type
γ: alist X
x: atom
hyp2: FV S k1 t1 ⊆ domset γ
H1: FV (T k2) k1 t2 ⊆ domset γ
?y ⊆ domset γ apply (FV_subst_upper_neq S); auto.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k1, k2: K
hyp1: k1 <> k2
t1: S LN
t2: T k2 LN
X: Type
γ: alist X
x: atom
hyp2: FV S k1 t1 ⊆ domset γ
H1: FV (T k2) k1 t2 ⊆ domset γ
FV S k1 t1 ∪ FV (T k2) k1 t2 ⊆ domset γ fsetdec.
  Qed.

  (** *** Other *)
  (******************************************************************************)
  Lemma scoped_envmap :
    forall (k : K) (t1 : S LN) (X Y : Type) (γ1 : alist X) (f : X -> Y),
      scoped S k t1 (domset γ1) ->
      scoped S k t1 (domset (envmap f γ1)).S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t1 : S LN) (X Y : Type) (γ1 : alist X)
  (f : X -> Y),
scoped S k t1 (domset γ1) ->
scoped S k t1 (domset (envmap f γ1))
  Proof.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
forall (k : K) (t1 : S LN) (X Y : Type) (γ1 : alist X)
  (f : X -> Y),
scoped S k t1 (domset γ1) ->
scoped S k t1 (domset (envmap f γ1))
    introv Hscope.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
X, Y: Type
γ1: alist X
f: X -> Y
Hscope: scoped S k t1 (domset γ1)
scoped S k t1 (domset (envmap f γ1)) unfold scoped in *.S: Type -> Type
ix: Index
T: K -> Type -> Type
MReturn0: MReturn T
MBind0: MBind (list K) T S
H: forall k : K, MBind (list K) T (T k)
H0: MultiDecoratedTraversablePreModule (list K) T S
MultiDecoratedTraversableMonad0: MultiDecoratedTraversableMonad
  (list K) T
k: K
t1: S LN
X, Y: Type
γ1: alist X
f: X -> Y
Hscope: FV S k t1 ⊆ domset γ1
FV S k t1 ⊆ domset (envmap f γ1)
    now rewrite domset_map.
  Qed.

End scope_lemmas.

(** * Infrastructural lemmas for contexts and well-formedness predicates *)
(******************************************************************************)

(** ** General properties of <<ok_kind_ctx>> *)
(******************************************************************************)
Lemma ok_kind_ctx_nil : forall x,
    ok_kind_ctx [].atom -> ok_kind_ctx []
Proof.atom -> ok_kind_ctx []
  intros.x: atom
ok_kind_ctx [] unfold ok_kind_ctx in *.x: atom
uniq []
  now bursts.
Qed.

Lemma ok_kind_ctx_one : forall x,
    ok_kind_ctx (x ~ tt).forall x, ok_kind_ctx (x ~ tt)
Proof.forall x, ok_kind_ctx (x ~ tt)
  intros.x: atom
ok_kind_ctx (x ~ tt) unfold ok_kind_ctx in *.x: atom
uniq (x ~ tt)
  now bursts.
Qed.

Lemma ok_kind_ctx_app : forall Δ1 Δ2,
    ok_kind_ctx (Δ1 ++ Δ2) <->
    ok_kind_ctx Δ1 /\ ok_kind_ctx Δ2 /\ disjoint Δ1 Δ2.forall Δ1 Δ2 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2) <->
ok_kind_ctx Δ1 /\ ok_kind_ctx Δ2 /\ disjoint Δ1 Δ2
Proof.forall Δ1 Δ2 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2) <->
ok_kind_ctx Δ1 /\ ok_kind_ctx Δ2 /\ disjoint Δ1 Δ2
  intros.Δ1, Δ2: list (atom * unit)
ok_kind_ctx (Δ1 ++ Δ2) <->
ok_kind_ctx Δ1 /\ ok_kind_ctx Δ2 /\ disjoint Δ1 Δ2 unfold ok_kind_ctx in *.Δ1, Δ2: list (atom * unit)
uniq (Δ1 ++ Δ2) <->
uniq Δ1 /\ uniq Δ2 /\ disjoint Δ1 Δ2
  now bursts.
Qed.

Lemma ok_kind_ctx_comm : forall Δ1 Δ2,
    ok_kind_ctx (Δ1 ++ Δ2) <->
    ok_kind_ctx (Δ1 ++ Δ2).forall Δ1 Δ2 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2) <-> ok_kind_ctx (Δ1 ++ Δ2)
Proof.forall Δ1 Δ2 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2) <-> ok_kind_ctx (Δ1 ++ Δ2)
  intros.Δ1, Δ2: list (atom * unit)
ok_kind_ctx (Δ1 ++ Δ2) <-> ok_kind_ctx (Δ1 ++ Δ2) unfold ok_kind_ctx.Δ1, Δ2: list (atom * unit)
uniq (Δ1 ++ Δ2) <-> uniq (Δ1 ++ Δ2) bursts.Δ1, Δ2: list (atom * unit)
uniq Δ1 /\ uniq Δ2 /\ disjoint Δ1 Δ2 <->
uniq Δ1 /\ uniq Δ2 /\ disjoint Δ1 Δ2
  rewrite disjoint_sym.Δ1, Δ2: list (atom * unit)
uniq Δ1 /\ uniq Δ2 /\ disjoint Δ2 Δ1 <->
uniq Δ1 /\ uniq Δ2 /\ disjoint Δ2 Δ1 firstorder.
Qed.

Lemma ok_kind_ctx_perm1 : forall Δ1 Δ2,
    ok_kind_ctx Δ1 ->
    Permutation Δ1 Δ2 ->
    ok_kind_ctx Δ2.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit)),
ok_kind_ctx Δ1 -> Permutation Δ1 Δ2 -> ok_kind_ctx Δ2
Proof.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit)),
ok_kind_ctx Δ1 -> Permutation Δ1 Δ2 -> ok_kind_ctx Δ2
  unfold ok_kind_ctx.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit)),
uniq Δ1 -> Permutation Δ1 Δ2 -> uniq Δ2 intros.Δ1: kind_ctx
Δ2: list (atom * unit)
H: uniq Δ1
H0: Permutation Δ1 Δ2
uniq Δ2 rewrite <- uniq_perm; eauto.
Qed.

Corollary ok_kind_ctx_perm : forall Δ1 Δ2,
    Permutation Δ1 Δ2 ->
    ok_kind_ctx Δ1 <-> ok_kind_ctx Δ2.forall Δ1 Δ2 : list (atom * unit),
Permutation Δ1 Δ2 -> ok_kind_ctx Δ1 <-> ok_kind_ctx Δ2
Proof.forall Δ1 Δ2 : list (atom * unit),
Permutation Δ1 Δ2 -> ok_kind_ctx Δ1 <-> ok_kind_ctx Δ2
  unfold ok_kind_ctx.forall Δ1 Δ2 : list (atom * unit),
Permutation Δ1 Δ2 -> uniq Δ1 <-> uniq Δ2 intros.Δ1, Δ2: list (atom * unit)
H: Permutation Δ1 Δ2
uniq Δ1 <-> uniq Δ2 now rewrite uniq_perm.
Qed.

#[export] Hint Resolve ok_kind_ctx_nil : sysf_ctx.
#[export] Hint Resolve ok_kind_ctx_one : sysf_ctx.
#[export] Hint Immediate ok_kind_ctx_perm1 : sysf_ctx.

(** ** Tactical support for <<ok_kind_ctx>> *)
(******************************************************************************)
Lemma ok_kind_ctx_app1 : forall Δ1 Δ2,
    ok_kind_ctx Δ1 /\ ok_kind_ctx Δ2 /\ disjoint Δ1 Δ2 ->
    ok_kind_ctx (Δ1 ++ Δ2).forall Δ1 Δ2 : kind_ctx,
ok_kind_ctx Δ1 /\ ok_kind_ctx Δ2 /\ disjoint Δ1 Δ2 ->
ok_kind_ctx (Δ1 ++ Δ2)
Proof.forall Δ1 Δ2 : kind_ctx,
ok_kind_ctx Δ1 /\ ok_kind_ctx Δ2 /\ disjoint Δ1 Δ2 ->
ok_kind_ctx (Δ1 ++ Δ2)
  intros.Δ1, Δ2: kind_ctx
H: ok_kind_ctx Δ1 /\ ok_kind_ctx Δ2 /\ disjoint Δ1 Δ2
ok_kind_ctx (Δ1 ++ Δ2) unfold ok_kind_ctx in *.Δ1, Δ2: kind_ctx
H: uniq Δ1 /\ uniq Δ2 /\ disjoint Δ1 Δ2
uniq (Δ1 ++ Δ2)
  now bursts.
Qed.

Lemma ok_kind_ctx_mid1: forall Δ1 Δ2 Δ3,
    ok_kind_ctx (Δ1 ++ Δ2 ++ Δ3) ->
    ok_kind_ctx Δ2.forall Δ1 Δ2 Δ3 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2 ++ Δ3) -> ok_kind_ctx Δ2
Proof.forall Δ1 Δ2 Δ3 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2 ++ Δ3) -> ok_kind_ctx Δ2
  intros.Δ1, Δ2, Δ3: list (atom * unit)
H: ok_kind_ctx (Δ1 ++ Δ2 ++ Δ3)
ok_kind_ctx Δ2 unfold ok_kind_ctx in *.Δ1, Δ2, Δ3: list (atom * unit)
H: uniq (Δ1 ++ Δ2 ++ Δ3)
uniq Δ2
  now bursts.
Qed.

Lemma ok_kind_ctx_mid2 : forall Δ1 Δ2 Δ3,
    ok_kind_ctx (Δ1 ++ Δ2 ++ Δ3) ->
    ok_kind_ctx (Δ1 ++ Δ3).forall Δ1 Δ2 Δ3 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2 ++ Δ3) -> ok_kind_ctx (Δ1 ++ Δ3)
Proof.forall Δ1 Δ2 Δ3 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2 ++ Δ3) -> ok_kind_ctx (Δ1 ++ Δ3)
  intros.Δ1, Δ2, Δ3: list (atom * unit)
H: ok_kind_ctx (Δ1 ++ Δ2 ++ Δ3)
ok_kind_ctx (Δ1 ++ Δ3) unfold ok_kind_ctx in *.Δ1, Δ2, Δ3: list (atom * unit)
H: uniq (Δ1 ++ Δ2 ++ Δ3)
uniq (Δ1 ++ Δ3)
  bursts.Δ1, Δ2, Δ3: list (atom * unit)
H: uniq Δ1 /\
(uniq Δ2 /\ uniq Δ3 /\ disjoint Δ2 Δ3) /\
disjoint Δ2 Δ1 /\ disjoint Δ3 Δ1
uniq Δ1 /\ uniq Δ3 /\ disjoint Δ1 Δ3 now rewrite disjoint_sym.
Qed.

Lemma ok_kind_ctx_app_l : forall Δ1 Δ2,
    ok_kind_ctx (Δ1 ++ Δ2) ->
    ok_kind_ctx Δ1.forall Δ1 Δ2 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2) -> ok_kind_ctx Δ1
Proof.forall Δ1 Δ2 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2) -> ok_kind_ctx Δ1
  intros.Δ1, Δ2: list (atom * unit)
H: ok_kind_ctx (Δ1 ++ Δ2)
ok_kind_ctx Δ1 unfold ok_kind_ctx in *.Δ1, Δ2: list (atom * unit)
H: uniq (Δ1 ++ Δ2)
uniq Δ1
  now bursts.
Qed.

Lemma ok_kind_ctx_app_r : forall Δ1 Δ2,
    ok_kind_ctx (Δ1 ++ Δ2) ->
    ok_kind_ctx Δ2.forall Δ1 Δ2 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2) -> ok_kind_ctx Δ2
Proof.forall Δ1 Δ2 : list (atom * unit),
ok_kind_ctx (Δ1 ++ Δ2) -> ok_kind_ctx Δ2
  intros.Δ1, Δ2: list (atom * unit)
H: ok_kind_ctx (Δ1 ++ Δ2)
ok_kind_ctx Δ2 unfold ok_kind_ctx in *.Δ1, Δ2: list (atom * unit)
H: uniq (Δ1 ++ Δ2)
uniq Δ2
  now bursts.
Qed.

#[export] Hint Resolve ok_kind_ctx_app1 : sysf_ctx.
#[export] Hint Immediate ok_kind_ctx_mid1 ok_kind_ctx_mid2 : sysf_ctx.
#[export] Hint Immediate ok_kind_ctx_app_l ok_kind_ctx_app_r : sysf_ctx.

(** ** General properties of <<ok_type>> *)
(******************************************************************************)

(** A well-formed type is locally closed. *)
Lemma ok_type_lc : forall Δ τ,
    ok_type Δ τ ->
    LC typ ktyp τ.forall (Δ : kind_ctx) (τ : typ LN),
ok_type Δ τ -> LC typ ktyp τ
Proof.forall (Δ : kind_ctx) (τ : typ LN),
ok_type Δ τ -> LC typ ktyp τ
  unfold ok_type.forall (Δ : kind_ctx) (τ : typ LN),
scoped typ ktyp τ (domset Δ) /\ LC typ ktyp τ ->
LC typ ktyp τ tauto.
Qed.

#[export] Hint Immediate ok_type_lc : sysf_ctx.
#[export] Hint Resolve ok_type_lc : sysf_ctx.

(** ** Structural properties of <<ok_type Δ τ>> in <<Δ>> *)
(******************************************************************************)

(** *** Permutation *)
(******************************************************************************)
Lemma ok_type_perm : forall Δ1 Δ2 τ,
    Permutation Δ1 Δ2 ->
    ok_type Δ1 τ <->
    ok_type Δ2 τ.forall (Δ1 Δ2 : list (atom * unit)) (τ : typ LN),
Permutation Δ1 Δ2 -> ok_type Δ1 τ <-> ok_type Δ2 τ
Proof.forall (Δ1 Δ2 : list (atom * unit)) (τ : typ LN),
Permutation Δ1 Δ2 -> ok_type Δ1 τ <-> ok_type Δ2 τ
  intros.Δ1, Δ2: list (atom * unit)
τ: typ LN
H: Permutation Δ1 Δ2
ok_type Δ1 τ <-> ok_type Δ2 τ unfold ok_type.Δ1, Δ2: list (atom * unit)
τ: typ LN
H: Permutation Δ1 Δ2
scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ <->
scoped typ ktyp τ (domset Δ2) /\ LC typ ktyp τ now rewrite (scoped_perm_iff); eauto.
Qed.

Lemma ok_type_perm1 : forall Δ1 Δ2 τ,
    ok_type Δ1 τ ->
    Permutation Δ1 Δ2 ->
    ok_type Δ2 τ.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (τ : typ LN),
ok_type Δ1 τ -> Permutation Δ1 Δ2 -> ok_type Δ2 τ
Proof.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (τ : typ LN),
ok_type Δ1 τ -> Permutation Δ1 Δ2 -> ok_type Δ2 τ
  intros.Δ1: kind_ctx
Δ2: list (atom * unit)
τ: typ LN
H: ok_type Δ1 τ
H0: Permutation Δ1 Δ2
ok_type Δ2 τ rewrite <- ok_type_perm; eauto.
Qed.

(** *** Weakening *)
Lemma ok_type_weak_r : forall Δ1 Δ2 τ,
    ok_type Δ1 τ ->
    ok_type (Δ1 ++ Δ2) τ.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (τ : typ LN), ok_type Δ1 τ -> ok_type (Δ1 ++ Δ2) τ
Proof.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (τ : typ LN), ok_type Δ1 τ -> ok_type (Δ1 ++ Δ2) τ
  unfold ok_type.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (τ : typ LN),
scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ ->
scoped typ ktyp τ (domset (Δ1 ++ Δ2)) /\ LC typ ktyp τ
  intros.Δ1: kind_ctx
Δ2: list (atom * unit)
τ: typ LN
H: scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ
scoped typ ktyp τ (domset (Δ1 ++ Δ2)) /\ LC typ ktyp τ split.Δ1: kind_ctx
Δ2: list (atom * unit)
τ: typ LN
H: scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ
scoped typ ktyp τ (domset (Δ1 ++ Δ2))
Δ1: kind_ctx
Δ2: list (atom * unit)
τ: typ LN
H: scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ
LC typ ktyp τ
  -Δ1: kind_ctx
Δ2: list (atom * unit)
τ: typ LN
H: scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ
scoped typ ktyp τ (domset (Δ1 ++ Δ2)) apply (scoped_weak_l typ).Δ1: kind_ctx
Δ2: list (atom * unit)
τ: typ LN
H: scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ
scoped typ ktyp τ (domset Δ1) tauto.
  -Δ1: kind_ctx
Δ2: list (atom * unit)
τ: typ LN
H: scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ
LC typ ktyp τ tauto.
Qed.

Lemma ok_type_weak_l : forall Δ1 Δ2 τ,
    ok_type Δ2 τ ->
    ok_type (Δ1 ++ Δ2) τ.forall (Δ1 : list (atom * unit)) (Δ2 : kind_ctx)
  (τ : typ LN), ok_type Δ2 τ -> ok_type (Δ1 ++ Δ2) τ
Proof.forall (Δ1 : list (atom * unit)) (Δ2 : kind_ctx)
  (τ : typ LN), ok_type Δ2 τ -> ok_type (Δ1 ++ Δ2) τ
  unfold ok_type.forall (Δ1 : list (atom * unit)) (Δ2 : kind_ctx)
  (τ : typ LN),
scoped typ ktyp τ (domset Δ2) /\ LC typ ktyp τ ->
scoped typ ktyp τ (domset (Δ1 ++ Δ2)) /\ LC typ ktyp τ intuition (auto using (scoped_weak_r typ)).
Qed.

(** *** Strengthening  *)
(******************************************************************************)
Lemma ok_type_stren : forall Δ1 Δ2 x τ,
    ok_type (Δ1 ++ x ~ tt ++ Δ2) τ ->
    ~ x `in` (FV typ ktyp τ) ->
    ok_type (Δ1 ++ Δ2) τ.forall (Δ1 Δ2 : list (atom * unit)) x (τ : typ LN),
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ ->
x `notin` FV typ ktyp τ -> ok_type (Δ1 ++ Δ2) τ
Proof.forall (Δ1 Δ2 : list (atom * unit)) x (τ : typ LN),
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ ->
x `notin` FV typ ktyp τ -> ok_type (Δ1 ++ Δ2) τ
  introv [? ?] ?.Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
H: scoped typ ktyp τ (domset (Δ1 ++ x ~ tt ++ Δ2))
H0: LC typ ktyp τ
H1: x `notin` FV typ ktyp τ
ok_type (Δ1 ++ Δ2) τ unfold ok_type.Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
H: scoped typ ktyp τ (domset (Δ1 ++ x ~ tt ++ Δ2))
H0: LC typ ktyp τ
H1: x `notin` FV typ ktyp τ
scoped typ ktyp τ (domset (Δ1 ++ Δ2)) /\ LC typ ktyp τ
  eauto using (scoped_stren_mid typ).
Qed.

Corollary ok_type_stren1 : forall Δ x τ,
    ok_type (Δ ++ x ~ tt) τ ->
    ~ x `in` (FV typ ktyp τ) ->
    ok_type Δ τ.forall (Δ : list (atom * unit)) x (τ : typ LN),
ok_type (Δ ++ x ~ tt) τ ->
x `notin` FV typ ktyp τ -> ok_type Δ τ
Proof.forall (Δ : list (atom * unit)) x (τ : typ LN),
ok_type (Δ ++ x ~ tt) τ ->
x `notin` FV typ ktyp τ -> ok_type Δ τ
  introv H1 H2.Δ: list (atom * unit)
x: atom
τ: typ LN
H1: ok_type (Δ ++ x ~ tt) τ
H2: x `notin` FV typ ktyp τ
ok_type Δ τ change_alist (Δ ++ x ~ tt ++ []) in H1.Δ: list (atom * unit)
x: atom
τ: typ LN
H1: ok_type (Δ ++ x ~ tt ++ []) τ
H2: x `notin` FV typ ktyp τ
ok_type Δ τ
  change_alist (Δ ++ []).Δ: list (atom * unit)
x: atom
τ: typ LN
H1: ok_type (Δ ++ x ~ tt ++ []) τ
H2: x `notin` FV typ ktyp τ
ok_type (Δ ++ []) τ eauto using ok_type_stren.
Qed.

(** *** Substitution *)
(******************************************************************************)
Lemma ok_type_sub : forall Δ1 Δ2 x τ1 τ2,
    ok_type (Δ1 ++ x ~ tt ++ Δ2) τ1 ->
    ok_type (Δ1 ++ Δ2) τ2 ->
    ok_type (Δ1 ++ Δ2) (subst typ ktyp x τ2 τ1).forall (Δ1 Δ2 : list (atom * unit)) x (τ1 τ2 : typ LN),
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ1 ->
ok_type (Δ1 ++ Δ2) τ2 ->
ok_type (Δ1 ++ Δ2) (subst typ ktyp x τ2 τ1)
Proof.forall (Δ1 Δ2 : list (atom * unit)) x (τ1 τ2 : typ LN),
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ1 ->
ok_type (Δ1 ++ Δ2) τ2 ->
ok_type (Δ1 ++ Δ2) (subst typ ktyp x τ2 τ1)
  unfold ok_type.forall (Δ1 Δ2 : list (atom * unit)) x (τ1 τ2 : typ LN),
scoped typ ktyp τ1 (domset (Δ1 ++ x ~ tt ++ Δ2)) /\
LC typ ktyp τ1 ->
scoped typ ktyp τ2 (domset (Δ1 ++ Δ2)) /\
LC typ ktyp τ2 ->
scoped typ ktyp (subst typ ktyp x τ2 τ1)
  (domset (Δ1 ++ Δ2)) /\
LC typ ktyp (subst typ ktyp x τ2 τ1) introv [? ?] [? ?].Δ1, Δ2: list (atom * unit)
x: atom
τ1, τ2: typ LN
H: scoped typ ktyp τ1 (domset (Δ1 ++ x ~ tt ++ Δ2))
H0: LC typ ktyp τ1
H1: scoped typ ktyp τ2 (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ2
scoped typ ktyp (subst typ ktyp x τ2 τ1)
  (domset (Δ1 ++ Δ2)) /\
LC typ ktyp (subst typ ktyp x τ2 τ1) split.Δ1, Δ2: list (atom * unit)
x: atom
τ1, τ2: typ LN
H: scoped typ ktyp τ1 (domset (Δ1 ++ x ~ tt ++ Δ2))
H0: LC typ ktyp τ1
H1: scoped typ ktyp τ2 (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ2
scoped typ ktyp (subst typ ktyp x τ2 τ1)
  (domset (Δ1 ++ Δ2))
Δ1, Δ2: list (atom * unit)
x: atom
τ1, τ2: typ LN
H: scoped typ ktyp τ1 (domset (Δ1 ++ x ~ tt ++ Δ2))
H0: LC typ ktyp τ1
H1: scoped typ ktyp τ2 (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ2
LC typ ktyp (subst typ ktyp x τ2 τ1)
  -Δ1, Δ2: list (atom * unit)
x: atom
τ1, τ2: typ LN
H: scoped typ ktyp τ1 (domset (Δ1 ++ x ~ tt ++ Δ2))
H0: LC typ ktyp τ1
H1: scoped typ ktyp τ2 (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ2
scoped typ ktyp (subst typ ktyp x τ2 τ1)
  (domset (Δ1 ++ Δ2)) pose (lemma := scoped_sub_eq_mid typ ktyp).Δ1, Δ2: list (atom * unit)
x: atom
τ1, τ2: typ LN
H: scoped typ ktyp τ1 (domset (Δ1 ++ x ~ tt ++ Δ2))
H0: LC typ ktyp τ1
H1: scoped typ ktyp τ2 (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ2
lemma:= scoped_sub_eq_mid typ ktyp: forall (t1 : typ LN) (t2 : SystemF ktyp LN)
  (X : Type) (γ1 γ2 : alist X) 
  x (x' : X),
scoped typ ktyp t1
  (domset (γ1 ++ x ~ x' ++ γ2)) ->
scoped (SystemF ktyp) ktyp t2
  (domset (γ1 ++ γ2)) ->
scoped typ ktyp (subst typ ktyp x t2 t1)
  (domset (γ1 ++ γ2))
scoped typ ktyp (subst typ ktyp x τ2 τ1)
  (domset (Δ1 ++ Δ2))
    eapply lemma; eassumption.
  -Δ1, Δ2: list (atom * unit)
x: atom
τ1, τ2: typ LN
H: scoped typ ktyp τ1 (domset (Δ1 ++ x ~ tt ++ Δ2))
H0: LC typ ktyp τ1
H1: scoped typ ktyp τ2 (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ2
LC typ ktyp (subst typ ktyp x τ2 τ1) auto using (subst_lc_eq typ).
Qed.

Corollary ok_type_sub1 : forall Δ x τ1 τ2,
    ok_type (Δ ++ x ~ tt) τ1 ->
    ok_type Δ τ2 ->
    ok_type Δ (subst typ ktyp x τ2 τ1).forall (Δ : list (atom * unit)) x (τ1 τ2 : typ LN),
ok_type (Δ ++ x ~ tt) τ1 ->
ok_type Δ τ2 -> ok_type Δ (subst typ ktyp x τ2 τ1)
Proof.forall (Δ : list (atom * unit)) x (τ1 τ2 : typ LN),
ok_type (Δ ++ x ~ tt) τ1 ->
ok_type Δ τ2 -> ok_type Δ (subst typ ktyp x τ2 τ1)
  introv H1 H2.Δ: list (atom * unit)
x: atom
τ1, τ2: typ LN
H1: ok_type (Δ ++ x ~ tt) τ1
H2: ok_type Δ τ2
ok_type Δ (subst typ ktyp x τ2 τ1) change_alist (Δ ++ x ~ tt ++ []) in H1.Δ: list (atom * unit)
x: atom
τ1, τ2: typ LN
H1: ok_type (Δ ++ x ~ tt ++ []) τ1
H2: ok_type Δ τ2
ok_type Δ (subst typ ktyp x τ2 τ1)
  change_alist (Δ ++ []) in H2.Δ: list (atom * unit)
x: atom
τ1, τ2: typ LN
H1: ok_type (Δ ++ x ~ tt ++ []) τ1
H2: ok_type (Δ ++ []) τ2
ok_type Δ (subst typ ktyp x τ2 τ1) change_alist (Δ ++ []).Δ: list (atom * unit)
x: atom
τ1, τ2: typ LN
H1: ok_type (Δ ++ x ~ tt ++ []) τ1
H2: ok_type (Δ ++ []) τ2
ok_type (Δ ++ []) (subst typ ktyp x τ2 τ1)
  auto using ok_type_sub.
Qed.

#[export] Hint Immediate ok_type_perm1 : sysf_ctx.
#[export] Hint Resolve ok_type_weak_l ok_type_weak_r : sysf_ctx.
#[export] Hint Immediate ok_type_stren ok_type_stren1 : sysf_ctx.
#[export] Hint Resolve ok_type_sub : sysf_ctx.
#[export] Hint Resolve ok_type_sub1 : sysf_ctx.

(** ** General properties of <<ok_type_ctx>> *)
(******************************************************************************)
Lemma ok_type_ctx_nil : forall Δ,
    ok_type_ctx Δ [].forall Δ : kind_ctx, ok_type_ctx Δ []
Proof.forall Δ : kind_ctx, ok_type_ctx Δ []
  intros.Δ: kind_ctx
ok_type_ctx Δ [] unfold ok_type_ctx in *.Δ: kind_ctx
uniq [] /\
(forall τ : typ LN, τ ∈ range [] -> ok_type Δ τ) now bursts.
Qed.

Lemma ok_type_ctx_cons : forall Δ Γ x τ,
    ok_type_ctx Δ Γ ->
    ~ (x `in` domset Γ) ->
    ok_type Δ τ ->
    ok_type_ctx Δ (x ~ τ ++ Γ).forall (Δ : kind_ctx) (Γ : type_ctx) x (τ : typ LN),
ok_type_ctx Δ Γ ->
x `notin` domset Γ ->
ok_type Δ τ -> ok_type_ctx Δ (x ~ τ ++ Γ)
Proof.forall (Δ : kind_ctx) (Γ : type_ctx) x (τ : typ LN),
ok_type_ctx Δ Γ ->
x `notin` domset Γ ->
ok_type Δ τ -> ok_type_ctx Δ (x ~ τ ++ Γ)
  intros.Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
H: ok_type_ctx Δ Γ
H0: x `notin` domset Γ
H1: ok_type Δ τ
ok_type_ctx Δ (x ~ τ ++ Γ) unfold ok_type_ctx in *.Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
H: uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ τ)
H0: x `notin` domset Γ
H1: ok_type Δ τ
uniq (x ~ τ ++ Γ) /\
(forall τ0 : typ LN,
 τ0 ∈ range (x ~ τ ++ Γ) -> ok_type Δ τ0) bursts.Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
H: uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ τ)
H0: x `notin` domset Γ
H1: ok_type Δ τ
(True /\ uniq Γ /\ x `notin` domset Γ) /\
(forall τ0 : typ LN,
 τ = τ0 \/ τ0 ∈ range Γ -> ok_type Δ τ0)
  splits.Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
H: uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ τ)
H0: x `notin` domset Γ
H1: ok_type Δ τ
True /\ uniq Γ /\ x `notin` domset Γ
Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
H: uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ τ)
H0: x `notin` domset Γ
H1: ok_type Δ τ
forall τ0 : typ LN,
τ = τ0 \/ τ0 ∈ range Γ -> ok_type Δ τ0
  -Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
H: uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ τ)
H0: x `notin` domset Γ
H1: ok_type Δ τ
True /\ uniq Γ /\ x `notin` domset Γ intuition.
  -Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
H: uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ τ)
H0: x `notin` domset Γ
H1: ok_type Δ τ
forall τ0 : typ LN,
τ = τ0 \/ τ0 ∈ range Γ -> ok_type Δ τ0 intros ? [?|?].Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
H: uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ τ)
H0: x `notin` domset Γ
H1: ok_type Δ τ
τ0: typ LN
H2: τ = τ0
ok_type Δ τ0
Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
H: uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ τ)
H0: x `notin` domset Γ
H1: ok_type Δ τ
τ0: typ LN
H2: τ0 ∈ range Γ
ok_type Δ τ0
    +Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
H: uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ τ)
H0: x `notin` domset Γ
H1: ok_type Δ τ
τ0: typ LN
H2: τ = τ0
ok_type Δ τ0 subst.Δ: kind_ctx
Γ: type_ctx
x: atom
H: uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ τ)
H0: x `notin` domset Γ
τ0: typ LN
H1: ok_type Δ τ0
ok_type Δ τ0 auto.
    +Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
H: uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ τ)
H0: x `notin` domset Γ
H1: ok_type Δ τ
τ0: typ LN
H2: τ0 ∈ range Γ
ok_type Δ τ0 firstorder.
Qed.

Lemma ok_type_ctx_one : forall Δ x τ,
    ok_type Δ τ ->
    ok_type_ctx Δ (x ~ τ).forall (Δ : kind_ctx) x (τ : typ LN),
ok_type Δ τ -> ok_type_ctx Δ (x ~ τ)
Proof.forall (Δ : kind_ctx) x (τ : typ LN),
ok_type Δ τ -> ok_type_ctx Δ (x ~ τ)
  intros.Δ: kind_ctx
x: atom
τ: typ LN
H: ok_type Δ τ
ok_type_ctx Δ (x ~ τ) change (x ~ τ) with [(x, τ)].Δ: kind_ctx
x: atom
τ: typ LN
H: ok_type Δ τ
ok_type_ctx Δ [(x, τ)]
  apply ok_type_ctx_cons; auto using ok_type_ctx_nil.Δ: kind_ctx
x: atom
τ: typ LN
H: ok_type Δ τ
x `notin` domset []
  fsetdec.
Qed.

Lemma ok_type_ctx_app : forall Δ Γ1 Γ2,
    ok_type_ctx Δ (Γ1 ++ Γ2) <->
    ok_type_ctx Δ Γ1 /\ ok_type_ctx Δ Γ2 /\ disjoint Γ1 Γ2.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)),
ok_type_ctx Δ (Γ1 ++ Γ2) <->
ok_type_ctx Δ Γ1 /\ ok_type_ctx Δ Γ2 /\ disjoint Γ1 Γ2
Proof.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)),
ok_type_ctx Δ (Γ1 ++ Γ2) <->
ok_type_ctx Δ Γ1 /\ ok_type_ctx Δ Γ2 /\ disjoint Γ1 Γ2
  intros.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
ok_type_ctx Δ (Γ1 ++ Γ2) <->
ok_type_ctx Δ Γ1 /\ ok_type_ctx Δ Γ2 /\ disjoint Γ1 Γ2 unfold ok_type_ctx.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
uniq (Γ1 ++ Γ2) /\
(forall τ : typ LN,
 τ ∈ range (Γ1 ++ Γ2) -> ok_type Δ τ) <->
(uniq Γ1 /\
 (forall τ : typ LN, τ ∈ range Γ1 -> ok_type Δ τ)) /\
(uniq Γ2 /\
 (forall τ : typ LN, τ ∈ range Γ2 -> ok_type Δ τ)) /\
disjoint Γ1 Γ2
  setoid_rewrite in_range_iff.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
uniq (Γ1 ++ Γ2) /\
(forall τ : typ LN,
 (exists x, (x, τ) ∈ (Γ1 ++ Γ2)) -> ok_type Δ τ) <->
(uniq Γ1 /\
 (forall τ : typ LN,
  (exists x, (x, τ) ∈ Γ1) -> ok_type Δ τ)) /\
(uniq Γ2 /\
 (forall τ : typ LN,
  (exists x, (x, τ) ∈ Γ2) -> ok_type Δ τ)) /\
disjoint Γ1 Γ2
  rewrite uniq_app_iff.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
(uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2) /\
(forall τ : typ LN,
 (exists x, (x, τ) ∈ (Γ1 ++ Γ2)) -> ok_type Δ τ) <->
(uniq Γ1 /\
 (forall τ : typ LN,
  (exists x, (x, τ) ∈ Γ1) -> ok_type Δ τ)) /\
(uniq Γ2 /\
 (forall τ : typ LN,
  (exists x, (x, τ) ∈ Γ2) -> ok_type Δ τ)) /\
disjoint Γ1 Γ2
  setoid_rewrite element_of_list_app.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
(uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2) /\
(forall τ : typ LN,
 (exists x, (x, τ) ∈ Γ1 \/ (x, τ) ∈ Γ2) -> ok_type Δ τ) <->
(uniq Γ1 /\
 (forall τ : typ LN,
  (exists x, (x, τ) ∈ Γ1) -> ok_type Δ τ)) /\
(uniq Γ2 /\
 (forall τ : typ LN,
  (exists x, (x, τ) ∈ Γ2) -> ok_type Δ τ)) /\
disjoint Γ1 Γ2
  firstorder.
Qed.

Lemma ok_type_ctx_app_comm : forall {Δ Γ1 Γ2},
    ok_type_ctx Δ (Γ1 ++ Γ2) <->
    ok_type_ctx Δ (Γ2 ++ Γ1).forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)),
ok_type_ctx Δ (Γ1 ++ Γ2) <-> ok_type_ctx Δ (Γ2 ++ Γ1)
Proof.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)),
ok_type_ctx Δ (Γ1 ++ Γ2) <-> ok_type_ctx Δ (Γ2 ++ Γ1)
  intros.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
ok_type_ctx Δ (Γ1 ++ Γ2) <-> ok_type_ctx Δ (Γ2 ++ Γ1) unfold ok_type_ctx.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
uniq (Γ1 ++ Γ2) /\
(forall τ : typ LN,
 τ ∈ range (Γ1 ++ Γ2) -> ok_type Δ τ) <->
uniq (Γ2 ++ Γ1) /\
(forall τ : typ LN,
 τ ∈ range (Γ2 ++ Γ1) -> ok_type Δ τ) bursts.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
(uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2) /\
(forall τ : typ LN,
 τ ∈ range Γ1 \/ τ ∈ range Γ2 -> ok_type Δ τ) <->
(uniq Γ2 /\ uniq Γ1 /\ disjoint Γ2 Γ1) /\
(forall τ : typ LN,
 τ ∈ range Γ2 \/ τ ∈ range Γ1 -> ok_type Δ τ)
  rewrite disjoint_sym.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
(uniq Γ1 /\ uniq Γ2 /\ disjoint Γ2 Γ1) /\
(forall τ : typ LN,
 τ ∈ range Γ1 \/ τ ∈ range Γ2 -> ok_type Δ τ) <->
(uniq Γ2 /\ uniq Γ1 /\ disjoint Γ2 Γ1) /\
(forall τ : typ LN,
 τ ∈ range Γ2 \/ τ ∈ range Γ1 -> ok_type Δ τ) firstorder.
Qed.

Lemma ok_type_ctx_binds : forall Δ Γ x τ,
    ok_type_ctx Δ Γ ->
    (x, τ) ∈ (Γ : list (atom * typ LN)) ->
    ok_type Δ τ.forall (Δ : kind_ctx) (Γ : type_ctx) x (τ : typ LN),
ok_type_ctx Δ Γ ->
(x, τ) ∈ (Γ : list (atom * typ LN)) -> ok_type Δ τ
Proof.forall (Δ : kind_ctx) (Γ : type_ctx) x (τ : typ LN),
ok_type_ctx Δ Γ ->
(x, τ) ∈ (Γ : list (atom * typ LN)) -> ok_type Δ τ
  introv Hok Hin.Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
Hok: ok_type_ctx Δ Γ
Hin: (x, τ) ∈ Γ
ok_type Δ τ unfold ok_type_ctx, ok_type in *.Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
Hok: uniq Γ /\
(forall τ : typ LN,
τ ∈ range Γ -> scoped typ ktyp τ (domset Δ) /\ LC typ ktyp τ)
Hin: (x, τ) ∈ Γ
scoped typ ktyp τ (domset Δ) /\ LC typ ktyp τ
  apply Hok.Δ: kind_ctx
Γ: type_ctx
x: atom
τ: typ LN
Hok: uniq Γ /\
(forall τ : typ LN,
τ ∈ range Γ -> scoped typ ktyp τ (domset Δ) /\ LC typ ktyp τ)
Hin: (x, τ) ∈ Γ
τ ∈ range Γ erewrite (in_range_iff Γ); eauto.
Qed.

(** <<ok_type_ctx Δ Γ>> supports permutation in Γ. *)
Lemma ok_type_ctx_perm_gamma1 : forall Δ Γ1 Γ2,
    ok_type_ctx Δ Γ1 ->
    Permutation Γ1 Γ2 ->
    ok_type_ctx Δ Γ2.forall (Δ : kind_ctx) (Γ1 : type_ctx)
  (Γ2 : list (atom * typ LN)),
ok_type_ctx Δ Γ1 ->
Permutation Γ1 Γ2 -> ok_type_ctx Δ Γ2
Proof.forall (Δ : kind_ctx) (Γ1 : type_ctx)
  (Γ2 : list (atom * typ LN)),
ok_type_ctx Δ Γ1 ->
Permutation Γ1 Γ2 -> ok_type_ctx Δ Γ2
  introv [huniq hok].Δ: kind_ctx
Γ1: type_ctx
Γ2: list (atom * typ LN)
huniq: uniq Γ1
hok: forall τ : typ LN, τ ∈ range Γ1 -> ok_type Δ τ
Permutation Γ1 Γ2 -> ok_type_ctx Δ Γ2 unfold ok_type_ctx in *.Δ: kind_ctx
Γ1: type_ctx
Γ2: list (atom * typ LN)
huniq: uniq Γ1
hok: forall τ : typ LN, τ ∈ range Γ1 -> ok_type Δ τ
Permutation Γ1 Γ2 ->
uniq Γ2 /\
(forall τ : typ LN, τ ∈ range Γ2 -> ok_type Δ τ) split.Δ: kind_ctx
Γ1: type_ctx
Γ2: list (atom * typ LN)
huniq: uniq Γ1
hok: forall τ : typ LN, τ ∈ range Γ1 -> ok_type Δ τ
H: Permutation Γ1 Γ2
uniq Γ2
Δ: kind_ctx
Γ1: type_ctx
Γ2: list (atom * typ LN)
huniq: uniq Γ1
hok: forall τ : typ LN, τ ∈ range Γ1 -> ok_type Δ τ
H: Permutation Γ1 Γ2
forall τ : typ LN, τ ∈ range Γ2 -> ok_type Δ τ
  -Δ: kind_ctx
Γ1: type_ctx
Γ2: list (atom * typ LN)
huniq: uniq Γ1
hok: forall τ : typ LN, τ ∈ range Γ1 -> ok_type Δ τ
H: Permutation Γ1 Γ2
uniq Γ2 rewrite uniq_perm; eauto.Δ: kind_ctx
Γ1: type_ctx
Γ2: list (atom * typ LN)
huniq: uniq Γ1
hok: forall τ : typ LN, τ ∈ range Γ1 -> ok_type Δ τ
H: Permutation Γ1 Γ2
Permutation Γ2 Γ1 now symmetry.
  -Δ: kind_ctx
Γ1: type_ctx
Γ2: list (atom * typ LN)
huniq: uniq Γ1
hok: forall τ : typ LN, τ ∈ range Γ1 -> ok_type Δ τ
H: Permutation Γ1 Γ2
forall τ : typ LN, τ ∈ range Γ2 -> ok_type Δ τ intros τ hin; specialize (hok τ).Δ: kind_ctx
Γ1: type_ctx
Γ2: list (atom * typ LN)
huniq: uniq Γ1
τ: typ LN
hok: τ ∈ range Γ1 -> ok_type Δ τ
H: Permutation Γ1 Γ2
hin: τ ∈ range Γ2
ok_type Δ τ
    apply hok.Δ: kind_ctx
Γ1: type_ctx
Γ2: list (atom * typ LN)
huniq: uniq Γ1
τ: typ LN
hok: τ ∈ range Γ1 -> ok_type Δ τ
H: Permutation Γ1 Γ2
hin: τ ∈ range Γ2
τ ∈ range Γ1 rewrite perm_range; eauto.
Qed.

Corollary ok_type_ctx_perm_gamma : forall Δ Γ1 Γ2,
    Permutation Γ1 Γ2 ->
    ok_type_ctx Δ Γ1 <-> ok_type_ctx Δ Γ2.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)),
Permutation Γ1 Γ2 ->
ok_type_ctx Δ Γ1 <-> ok_type_ctx Δ Γ2
Proof.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)),
Permutation Γ1 Γ2 ->
ok_type_ctx Δ Γ1 <-> ok_type_ctx Δ Γ2
  introv Hperm; split; intro.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
Hperm: Permutation Γ1 Γ2
H: ok_type_ctx Δ Γ1
ok_type_ctx Δ Γ2
Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
Hperm: Permutation Γ1 Γ2
H: ok_type_ctx Δ Γ2
ok_type_ctx Δ Γ1
  -Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
Hperm: Permutation Γ1 Γ2
H: ok_type_ctx Δ Γ1
ok_type_ctx Δ Γ2 eauto using ok_type_ctx_perm_gamma1.
  -Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
Hperm: Permutation Γ1 Γ2
H: ok_type_ctx Δ Γ2
ok_type_ctx Δ Γ1 symmetry in Hperm.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
Hperm: Permutation Γ2 Γ1
H: ok_type_ctx Δ Γ2
ok_type_ctx Δ Γ1 eauto using ok_type_ctx_perm_gamma1.
Qed.

#[export] Hint Resolve ok_type_ctx_nil : sysf_ctx.
#[export] Hint Resolve ok_type_ctx_cons : sysf_ctx.
#[export] Hint Resolve ok_type_ctx_one : sysf_ctx.
#[export] Hint Immediate ok_type_ctx_app_comm : sysf_ctx.
#[export] Hint Immediate ok_type_ctx_binds : sysf_ctx.
#[export] Hint Immediate ok_type_ctx_perm_gamma : sysf_ctx.

(** ** Tactical support for <<ok_type_ctx>> *)
(******************************************************************************)
Lemma ok_type_ctx_inv_app_l : forall Δ Γ1 Γ2,
    ok_type_ctx Δ (Γ1 ++ Γ2) ->
    ok_type_ctx Δ Γ1.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)),
ok_type_ctx Δ (Γ1 ++ Γ2) -> ok_type_ctx Δ Γ1
Proof.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)),
ok_type_ctx Δ (Γ1 ++ Γ2) -> ok_type_ctx Δ Γ1
  introv [huniq hscope].Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
huniq: uniq (Γ1 ++ Γ2)
hscope: forall τ : typ LN,
τ ∈ range (Γ1 ++ Γ2) -> ok_type Δ τ
ok_type_ctx Δ Γ1 unfold ok_type_ctx in *.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
huniq: uniq (Γ1 ++ Γ2)
hscope: forall τ : typ LN,
τ ∈ range (Γ1 ++ Γ2) -> ok_type Δ τ
uniq Γ1 /\
(forall τ : typ LN, τ ∈ range Γ1 -> ok_type Δ τ)
  bursts.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
huniq: uniq Γ1 /\ uniq Γ2 /\ disjoint Γ1 Γ2
hscope: forall τ : typ LN,
τ ∈ range Γ1 \/ τ ∈ range Γ2 -> ok_type Δ τ
uniq Γ1 /\
(forall τ : typ LN, τ ∈ range Γ1 -> ok_type Δ τ) firstorder.
Qed.

Corollary ok_type_ctx_inv_app_r : forall Δ Γ1 Γ2,
    ok_type_ctx Δ (Γ1 ++ Γ2) ->
    ok_type_ctx Δ Γ2.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)),
ok_type_ctx Δ (Γ1 ++ Γ2) -> ok_type_ctx Δ Γ2
Proof.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)),
ok_type_ctx Δ (Γ1 ++ Γ2) -> ok_type_ctx Δ Γ2
  introv hyp.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
hyp: ok_type_ctx Δ (Γ1 ++ Γ2)
ok_type_ctx Δ Γ2 rewrite ok_type_ctx_app_comm in hyp.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
hyp: ok_type_ctx Δ (Γ2 ++ Γ1)
ok_type_ctx Δ Γ2
  eauto using ok_type_ctx_inv_app_l.
Qed.

Corollary ok_type_ctx_inv_mid : forall Δ Γ1 Γ2 Γ3,
    ok_type_ctx Δ (Γ1 ++ Γ2 ++ Γ3) ->
    ok_type_ctx Δ (Γ1 ++ Γ3).forall (Δ : kind_ctx)
  (Γ1 Γ2 Γ3 : list (atom * typ LN)),
ok_type_ctx Δ (Γ1 ++ Γ2 ++ Γ3) ->
ok_type_ctx Δ (Γ1 ++ Γ3)
Proof.forall (Δ : kind_ctx)
  (Γ1 Γ2 Γ3 : list (atom * typ LN)),
ok_type_ctx Δ (Γ1 ++ Γ2 ++ Γ3) ->
ok_type_ctx Δ (Γ1 ++ Γ3)
  introv hyp.Δ: kind_ctx
Γ1, Γ2, Γ3: list (atom * typ LN)
hyp: ok_type_ctx Δ (Γ1 ++ Γ2 ++ Γ3)
ok_type_ctx Δ (Γ1 ++ Γ3)
  change_alist ((Γ1 ++ Γ2) ++ Γ3) in hyp.Δ: kind_ctx
Γ1, Γ2, Γ3: list (atom * typ LN)
hyp: ok_type_ctx Δ ((Γ1 ++ Γ2) ++ Γ3)
ok_type_ctx Δ (Γ1 ++ Γ3)
  rewrite ok_type_ctx_app_comm in hyp.Δ: kind_ctx
Γ1, Γ2, Γ3: list (atom * typ LN)
hyp: ok_type_ctx Δ (Γ3 ++ Γ1 ++ Γ2)
ok_type_ctx Δ (Γ1 ++ Γ3)
  change_alist ((Γ3 ++ Γ1) ++ Γ2) in hyp.Δ: kind_ctx
Γ1, Γ2, Γ3: list (atom * typ LN)
hyp: ok_type_ctx Δ ((Γ3 ++ Γ1) ++ Γ2)
ok_type_ctx Δ (Γ1 ++ Γ3)
  apply ok_type_ctx_inv_app_l in hyp.Δ: kind_ctx
Γ1, Γ2, Γ3: list (atom * typ LN)
hyp: ok_type_ctx Δ (Γ3 ++ Γ1)
ok_type_ctx Δ (Γ1 ++ Γ3)
  now rewrite ok_type_ctx_app_comm in hyp.
Qed.

#[export] Hint Immediate ok_type_ctx_inv_app_l : sysf_ctx.
#[export] Hint Immediate ok_type_ctx_inv_app_r : sysf_ctx.
#[export] Hint Immediate ok_type_ctx_inv_mid : sysf_ctx.

(** ** Structural properties in <<Δ>> in <<ok_type_ctx Δ Γ>>. *)
(******************************************************************************)

(** *** Permutation *)
(******************************************************************************)
Theorem ok_type_ctx_perm1 : forall Δ1 Δ2 Γ,
    ok_type_ctx Δ1 Γ ->
    Permutation Δ1 Δ2 ->
    ok_type_ctx Δ2 Γ.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (Γ : type_ctx),
ok_type_ctx Δ1 Γ ->
Permutation Δ1 Δ2 -> ok_type_ctx Δ2 Γ
Proof.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (Γ : type_ctx),
ok_type_ctx Δ1 Γ ->
Permutation Δ1 Δ2 -> ok_type_ctx Δ2 Γ
  introv [? ?] ?.Δ1: kind_ctx
Δ2: list (atom * unit)
Γ: type_ctx
H: uniq Γ
H0: forall τ : typ LN, τ ∈ range Γ -> ok_type Δ1 τ
H1: Permutation Δ1 Δ2
ok_type_ctx Δ2 Γ unfold ok_type_ctx.Δ1: kind_ctx
Δ2: list (atom * unit)
Γ: type_ctx
H: uniq Γ
H0: forall τ : typ LN, τ ∈ range Γ -> ok_type Δ1 τ
H1: Permutation Δ1 Δ2
uniq Γ /\
(forall τ : typ LN, τ ∈ range Γ -> ok_type Δ2 τ)
  split; eauto using ok_type_perm1 with tea_alist.
Qed.

Corollary ok_type_ctx_perm : forall Δ1 Δ2 Γ,
    Permutation Δ1 Δ2 ->
    ok_type_ctx Δ1 Γ <-> ok_type_ctx Δ2 Γ.forall (Δ1 Δ2 : list (atom * unit)) (Γ : type_ctx),
Permutation Δ1 Δ2 ->
ok_type_ctx Δ1 Γ <-> ok_type_ctx Δ2 Γ
Proof.forall (Δ1 Δ2 : list (atom * unit)) (Γ : type_ctx),
Permutation Δ1 Δ2 ->
ok_type_ctx Δ1 Γ <-> ok_type_ctx Δ2 Γ
  introv Hperm.Δ1, Δ2: list (atom * unit)
Γ: type_ctx
Hperm: Permutation Δ1 Δ2
ok_type_ctx Δ1 Γ <-> ok_type_ctx Δ2 Γ unfold ok_type_ctx, ok_type.Δ1, Δ2: list (atom * unit)
Γ: type_ctx
Hperm: Permutation Δ1 Δ2
uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ ->
 scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ) <->
uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ ->
 scoped typ ktyp τ (domset Δ2) /\ LC typ ktyp τ)
  split; intros.Δ1, Δ2: list (atom * unit)
Γ: type_ctx
Hperm: Permutation Δ1 Δ2
H: uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ ->
 scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ)
uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ ->
 scoped typ ktyp τ (domset Δ2) /\ LC typ ktyp τ)
Δ1, Δ2: list (atom * unit)
Γ: type_ctx
Hperm: Permutation Δ1 Δ2
H: uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ ->
 scoped typ ktyp τ (domset Δ2) /\ LC typ ktyp τ)
uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ ->
 scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ)
  -Δ1, Δ2: list (atom * unit)
Γ: type_ctx
Hperm: Permutation Δ1 Δ2
H: uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ ->
 scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ)
uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ ->
 scoped typ ktyp τ (domset Δ2) /\ LC typ ktyp τ) eapply ok_type_ctx_perm1; eauto.
  -Δ1, Δ2: list (atom * unit)
Γ: type_ctx
Hperm: Permutation Δ1 Δ2
H: uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ ->
 scoped typ ktyp τ (domset Δ2) /\ LC typ ktyp τ)
uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ ->
 scoped typ ktyp τ (domset Δ1) /\ LC typ ktyp τ) eapply ok_type_ctx_perm1; eauto.Δ1, Δ2: list (atom * unit)
Γ: type_ctx
Hperm: Permutation Δ1 Δ2
H: uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ ->
 scoped typ ktyp τ (domset Δ2) /\ LC typ ktyp τ)
Permutation Δ2 Δ1
    now apply Permutation_sym.
Qed.

#[local] Set Firstorder Depth 4.

(** *** Weakening *)
(******************************************************************************)
Lemma ok_type_ctx_weak_r : forall Δ1 Δ2 Γ,
    ok_type_ctx Δ1 Γ ->
    ok_type_ctx (Δ1 ++ Δ2) Γ.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (Γ : type_ctx),
ok_type_ctx Δ1 Γ -> ok_type_ctx (Δ1 ++ Δ2) Γ
Proof.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (Γ : type_ctx),
ok_type_ctx Δ1 Γ -> ok_type_ctx (Δ1 ++ Δ2) Γ
  introv [huniq hok1].Δ1: kind_ctx
Δ2: list (atom * unit)
Γ: type_ctx
huniq: uniq Γ
hok1: forall τ : typ LN, τ ∈ range Γ -> ok_type Δ1 τ
ok_type_ctx (Δ1 ++ Δ2) Γ unfold ok_type_ctx in *.Δ1: kind_ctx
Δ2: list (atom * unit)
Γ: type_ctx
huniq: uniq Γ
hok1: forall τ : typ LN, τ ∈ range Γ -> ok_type Δ1 τ
uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ -> ok_type (Δ1 ++ Δ2) τ)
  firstorder using ok_type_weak_r.
Qed.

(** *** Strengthening *)
(******************************************************************************)
Lemma ok_type_ctx_stren : forall Δ1 Δ2 x Γ,
    ok_type_ctx (Δ1 ++ x ~ tt ++ Δ2) Γ ->
    (forall t : typ LN, t ∈ range Γ -> ~ x `in` FV typ ktyp t) ->
    ok_type_ctx (Δ1 ++ Δ2) Γ.forall (Δ1 Δ2 : list (atom * unit)) x (Γ : type_ctx),
ok_type_ctx (Δ1 ++ x ~ tt ++ Δ2) Γ ->
(forall t : typ LN,
 t ∈ range Γ -> x `notin` FV typ ktyp t) ->
ok_type_ctx (Δ1 ++ Δ2) Γ
Proof.forall (Δ1 Δ2 : list (atom * unit)) x (Γ : type_ctx),
ok_type_ctx (Δ1 ++ x ~ tt ++ Δ2) Γ ->
(forall t : typ LN,
 t ∈ range Γ -> x `notin` FV typ ktyp t) ->
ok_type_ctx (Δ1 ++ Δ2) Γ
  introv [hunit hok] hfresh.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
hfresh: forall t : typ LN,
t ∈ range Γ -> x `notin` FV typ ktyp t
ok_type_ctx (Δ1 ++ Δ2) Γ
  unfold ok_type_ctx.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
hfresh: forall t : typ LN,
t ∈ range Γ -> x `notin` FV typ ktyp t
uniq Γ /\
(forall τ : typ LN,
 τ ∈ range Γ -> ok_type (Δ1 ++ Δ2) τ) split; [trivial |].Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
hfresh: forall t : typ LN,
t ∈ range Γ -> x `notin` FV typ ktyp t
forall τ : typ LN, τ ∈ range Γ -> ok_type (Δ1 ++ Δ2) τ
  intros τ hin; specialize (hok τ hin).Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
hunit: uniq Γ
τ: typ LN
hok: ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
hfresh: forall t : typ LN,
t ∈ range Γ -> x `notin` FV typ ktyp t
hin: τ ∈ range Γ
ok_type (Δ1 ++ Δ2) τ
  eauto using ok_type_stren.
Qed.

Corollary ok_type_ctx_stren1 : forall Δ x Γ,
    ok_type_ctx (Δ ++ x ~ tt) Γ ->
    (forall t : typ LN, t ∈ range Γ -> ~ x `in` FV typ ktyp t) ->
    ok_type_ctx Δ Γ.forall (Δ : list (atom * unit)) x (Γ : type_ctx),
ok_type_ctx (Δ ++ x ~ tt) Γ ->
(forall t : typ LN,
 t ∈ range Γ -> x `notin` FV typ ktyp t) ->
ok_type_ctx Δ Γ
Proof.forall (Δ : list (atom * unit)) x (Γ : type_ctx),
ok_type_ctx (Δ ++ x ~ tt) Γ ->
(forall t : typ LN,
 t ∈ range Γ -> x `notin` FV typ ktyp t) ->
ok_type_ctx Δ Γ
  introv hyp1 hyp2.Δ: list (atom * unit)
x: atom
Γ: type_ctx
hyp1: ok_type_ctx (Δ ++ x ~ tt) Γ
hyp2: forall t : typ LN,
t ∈ range Γ -> x `notin` FV typ ktyp t
ok_type_ctx Δ Γ change_alist (Δ ++ x ~ tt ++ []) in hyp1.Δ: list (atom * unit)
x: atom
Γ: type_ctx
hyp1: ok_type_ctx (Δ ++ x ~ tt ++ []) Γ
hyp2: forall t : typ LN,
t ∈ range Γ -> x `notin` FV typ ktyp t
ok_type_ctx Δ Γ
  change_alist (Δ ++ []).Δ: list (atom * unit)
x: atom
Γ: type_ctx
hyp1: ok_type_ctx (Δ ++ x ~ tt ++ []) Γ
hyp2: forall t : typ LN,
t ∈ range Γ -> x `notin` FV typ ktyp t
ok_type_ctx (Δ ++ []) Γ eauto using ok_type_ctx_stren.
Qed.

Lemma ok_type_ctx_sub : forall Δ1 Δ2 x Γ τ,
    ok_type_ctx (Δ1 ++ x ~ tt ++ Δ2) Γ ->
    ok_type (Δ1 ++ Δ2) τ ->
    LC typ ktyp τ ->
    ok_type_ctx (Δ1 ++ Δ2) (envmap (subst typ ktyp x τ) Γ).forall (Δ1 Δ2 : list (atom * unit)) x (Γ : type_ctx)
  (τ : typ LN),
ok_type_ctx (Δ1 ++ x ~ tt ++ Δ2) Γ ->
ok_type (Δ1 ++ Δ2) τ ->
LC typ ktyp τ ->
ok_type_ctx (Δ1 ++ Δ2) (envmap (subst typ ktyp x τ) Γ)
Proof.forall (Δ1 Δ2 : list (atom * unit)) x (Γ : type_ctx)
  (τ : typ LN),
ok_type_ctx (Δ1 ++ x ~ tt ++ Δ2) Γ ->
ok_type (Δ1 ++ Δ2) τ ->
LC typ ktyp τ ->
ok_type_ctx (Δ1 ++ Δ2) (envmap (subst typ ktyp x τ) Γ)
  introv [hunit hok] Hscope lc.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
ok_type_ctx (Δ1 ++ Δ2) (envmap (subst typ ktyp x τ) Γ) unfold ok_type_ctx.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
uniq (envmap (subst typ ktyp x τ) Γ) /\
(forall τ0 : typ LN,
 τ0 ∈ range (envmap (subst typ ktyp x τ) Γ) ->
 ok_type (Δ1 ++ Δ2) τ0) split.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
uniq (envmap (subst typ ktyp x τ) Γ)
Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
forall τ0 : typ LN,
τ0 ∈ range (envmap (subst typ ktyp x τ) Γ) ->
ok_type (Δ1 ++ Δ2) τ0
  -Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
uniq (envmap (subst typ ktyp x τ) Γ) now apply uniq_map2.
  -Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
forall τ0 : typ LN,
τ0 ∈ range (envmap (subst typ ktyp x τ) Γ) ->
ok_type (Δ1 ++ Δ2) τ0 intros τ2 τ2in.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
τ2: typ LN
τ2in: τ2 ∈ range (envmap (subst typ ktyp x τ) Γ)
ok_type (Δ1 ++ Δ2) τ2
    rewrite in_range_iff in τ2in.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
τ2: typ LN
τ2in: exists x0,
  (x0, τ2) ∈ envmap (subst typ ktyp x τ) Γ
ok_type (Δ1 ++ Δ2) τ2
    setoid_rewrite in_envmap_iff in τ2in.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
τ2: typ LN
τ2in: exists x0 (a : typ LN),
  (x0, a) ∈ Γ /\ subst typ ktyp x τ a = τ2
ok_type (Δ1 ++ Δ2) τ2
    destruct τ2in as [y [τ2_inv [? ?]]]; subst.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
hok: forall τ : typ LN,
τ ∈ range Γ -> ok_type (Δ1 ++ x ~ tt ++ Δ2) τ
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
y: atom
τ2_inv: typ LN
H: (y, τ2_inv) ∈ Γ
ok_type (Δ1 ++ Δ2) (subst typ ktyp x τ τ2_inv)
    specialize (hok τ2_inv).Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
τ2_inv: typ LN
hok: τ2_inv ∈ range Γ ->
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ2_inv
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
y: atom
H: (y, τ2_inv) ∈ Γ
ok_type (Δ1 ++ Δ2) (subst typ ktyp x τ τ2_inv)
    apply ok_type_sub.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
τ2_inv: typ LN
hok: τ2_inv ∈ range Γ ->
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ2_inv
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
y: atom
H: (y, τ2_inv) ∈ Γ
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ2_inv
Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
τ2_inv: typ LN
hok: τ2_inv ∈ range Γ ->
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ2_inv
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
y: atom
H: (y, τ2_inv) ∈ Γ
ok_type (Δ1 ++ Δ2) τ
    +Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
τ2_inv: typ LN
hok: τ2_inv ∈ range Γ ->
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ2_inv
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
y: atom
H: (y, τ2_inv) ∈ Γ
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ2_inv apply hok.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
τ2_inv: typ LN
hok: τ2_inv ∈ range Γ ->
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ2_inv
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
y: atom
H: (y, τ2_inv) ∈ Γ
τ2_inv ∈ range Γ rewrite in_range_iff.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
τ2_inv: typ LN
hok: τ2_inv ∈ range Γ ->
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ2_inv
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
y: atom
H: (y, τ2_inv) ∈ Γ
exists x, (x, τ2_inv) ∈ Γ eauto.
    +Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
τ: typ LN
hunit: uniq Γ
τ2_inv: typ LN
hok: τ2_inv ∈ range Γ ->
ok_type (Δ1 ++ x ~ tt ++ Δ2) τ2_inv
Hscope: ok_type (Δ1 ++ Δ2) τ
lc: LC typ ktyp τ
y: atom
H: (y, τ2_inv) ∈ Γ
ok_type (Δ1 ++ Δ2) τ auto.
Qed.

#[export] Hint Immediate ok_type_ctx_perm : sysf_ctx.
#[export] Hint Resolve ok_type_ctx_perm1 : sysf_ctx.
#[export] Hint Resolve ok_type_ctx_weak_r : sysf_ctx.
#[export] Hint Resolve ok_type_ctx_sub : sysf_ctx.

(** ** Structural properties of <<ok_term Δ Γ t>> in <<Δ>> *)
(******************************************************************************)

(** *** Permutation *)
(******************************************************************************)
Lemma ok_term_perm_delta : forall Δ1 Δ2 Γ t,
    Permutation Δ1 Δ2 ->
    ok_term Δ1 Γ t <->
    ok_term Δ2 Γ t.forall (Δ1 Δ2 : list (atom * unit)) (Γ : type_ctx)
  (t : term LN),
Permutation Δ1 Δ2 -> ok_term Δ1 Γ t <-> ok_term Δ2 Γ t
Proof.forall (Δ1 Δ2 : list (atom * unit)) (Γ : type_ctx)
  (t : term LN),
Permutation Δ1 Δ2 -> ok_term Δ1 Γ t <-> ok_term Δ2 Γ t
  intros.Δ1, Δ2: list (atom * unit)
Γ: type_ctx
t: term LN
H: Permutation Δ1 Δ2
ok_term Δ1 Γ t <-> ok_term Δ2 Γ t unfold ok_term.Δ1, Δ2: list (atom * unit)
Γ: type_ctx
t: term LN
H: Permutation Δ1 Δ2
scoped term ktyp t (domset Δ1) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t <->
scoped term ktyp t (domset Δ2) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t
  now rewrite scoped_perm_iff.
Qed.

(** *** Weakening *)
(******************************************************************************)
Lemma ok_term_weak_delta_r : forall Δ1 Δ2 Γ t,
    ok_term Δ1 Γ t ->
    ok_term (Δ1 ++ Δ2) Γ t.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (Γ : type_ctx) (t : term LN),
ok_term Δ1 Γ t -> ok_term (Δ1 ++ Δ2) Γ t
Proof.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (Γ : type_ctx) (t : term LN),
ok_term Δ1 Γ t -> ok_term (Δ1 ++ Δ2) Γ t
  unfold ok_term.forall (Δ1 : kind_ctx) (Δ2 : list (atom * unit))
  (Γ : type_ctx) (t : term LN),
scoped term ktyp t (domset Δ1) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t ->
scoped term ktyp t (domset (Δ1 ++ Δ2)) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t intros.Δ1: kind_ctx
Δ2: list (atom * unit)
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset Δ1) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t
scoped term ktyp t (domset (Δ1 ++ Δ2)) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t
  intuition (eauto using (scoped_weak_l term)).
Qed.

Lemma ok_term_weak_delta_l : forall Δ1 Δ2 Γ t,
    ok_term Δ2 Γ t ->
    ok_term (Δ1 ++ Δ2) Γ t.forall (Δ1 : list (atom * unit)) (Δ2 : kind_ctx)
  (Γ : type_ctx) (t : term LN),
ok_term Δ2 Γ t -> ok_term (Δ1 ++ Δ2) Γ t
Proof.forall (Δ1 : list (atom * unit)) (Δ2 : kind_ctx)
  (Γ : type_ctx) (t : term LN),
ok_term Δ2 Γ t -> ok_term (Δ1 ++ Δ2) Γ t
  unfold ok_term.forall (Δ1 : list (atom * unit)) (Δ2 : kind_ctx)
  (Γ : type_ctx) (t : term LN),
scoped term ktyp t (domset Δ2) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t ->
scoped term ktyp t (domset (Δ1 ++ Δ2)) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t intros.Δ1: list (atom * unit)
Δ2: kind_ctx
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset Δ2) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t
scoped term ktyp t (domset (Δ1 ++ Δ2)) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t
  intuition (eauto using (scoped_weak_r term)).
Qed.

(** *** Strengthening  *)
(******************************************************************************)
Lemma ok_term_stren_delta : forall Δ1 Δ2 x Γ t,
    ok_term (Δ1 ++ x ~ tt ++ Δ2) Γ t ->
    ~ x `in` (FV term ktyp t) ->
    ok_term (Δ1 ++ Δ2) Γ t.forall (Δ1 Δ2 : list (atom * unit)) x (Γ : type_ctx)
  (t : term LN),
ok_term (Δ1 ++ x ~ tt ++ Δ2) Γ t ->
x `notin` FV term ktyp t -> ok_term (Δ1 ++ Δ2) Γ t
Proof.forall (Δ1 Δ2 : list (atom * unit)) x (Γ : type_ctx)
  (t : term LN),
ok_term (Δ1 ++ x ~ tt ++ Δ2) Γ t ->
x `notin` FV term ktyp t -> ok_term (Δ1 ++ Δ2) Γ t
  introv Hok Hfresh.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
t: term LN
Hok: ok_term (Δ1 ++ x ~ tt ++ Δ2) Γ t
Hfresh: x `notin` FV term ktyp t
ok_term (Δ1 ++ Δ2) Γ t unfold ok_term in *.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
t: term LN
Hok: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2)) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t
Hfresh: x `notin` FV term ktyp t
scoped term ktyp t (domset (Δ1 ++ Δ2)) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t
  intuition.Δ1, Δ2: list (atom * unit)
x: atom
Γ: type_ctx
t: term LN
Hfresh: x `in` FV term ktyp t -> False
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H3: LC term ktyp t
scoped term ktyp t (domset (Δ1 ++ Δ2)) eapply (scoped_stren_mid term); eauto.
Qed.

(** *** Substitution *)
(******************************************************************************)
Lemma ok_term_sub_delta : forall Δ1 Δ2 x τ Γ t,
    ok_term (Δ1 ++ x ~ tt ++ Δ2) Γ t ->
    ok_type (Δ1 ++ Δ2) τ ->
    ok_term (Δ1 ++ Δ2) (envmap (subst typ ktyp x τ) Γ) (subst term ktyp x τ t).forall (Δ1 Δ2 : list (atom * unit)) x (τ : typ LN)
  (Γ : type_ctx) (t : term LN),
ok_term (Δ1 ++ x ~ tt ++ Δ2) Γ t ->
ok_type (Δ1 ++ Δ2) τ ->
ok_term (Δ1 ++ Δ2) (envmap (subst typ ktyp x τ) Γ)
  (subst term ktyp x τ t)
Proof.forall (Δ1 Δ2 : list (atom * unit)) x (τ : typ LN)
  (Γ : type_ctx) (t : term LN),
ok_term (Δ1 ++ x ~ tt ++ Δ2) Γ t ->
ok_type (Δ1 ++ Δ2) τ ->
ok_term (Δ1 ++ Δ2) (envmap (subst typ ktyp x τ) Γ)
  (subst term ktyp x τ t)
  introv Hokt Hokτ.Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
Hokt: ok_term (Δ1 ++ x ~ tt ++ Δ2) Γ t
Hokτ: ok_type (Δ1 ++ Δ2) τ
ok_term (Δ1 ++ Δ2) (envmap (subst typ ktyp x τ) Γ)
  (subst term ktyp x τ t) unfold ok_term, ok_type in *.Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
Hokt: scoped term ktyp t
  (domset (Δ1 ++ x ~ tt ++ Δ2)) /\
scoped term ktrm t (domset Γ) /\
LC term ktrm t /\ LC term ktyp t
Hokτ: scoped typ ktyp τ (domset (Δ1 ++ Δ2)) /\
LC typ ktyp τ
scoped term ktyp (subst term ktyp x τ t)
  (domset (Δ1 ++ Δ2)) /\
scoped term ktrm (subst term ktyp x τ t)
  (domset (envmap (subst typ ktyp x τ) Γ)) /\
LC term ktrm (subst term ktyp x τ t) /\
LC term ktyp (subst term ktyp x τ t)
  intuition.Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
scoped term ktyp (subst term ktyp x τ t)
  (domset (Δ1 ++ Δ2))
Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
scoped term ktrm (subst term ktyp x τ t)
  (domset (envmap (subst typ ktyp x τ) Γ))
Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
LC term ktrm (subst term ktyp x τ t)
Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
LC term ktyp (subst term ktyp x τ t)
  -Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
scoped term ktyp (subst term ktyp x τ t)
  (domset (Δ1 ++ Δ2)) eapply (scoped_sub_eq_mid term); eauto.
  -Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
scoped term ktrm (subst term ktyp x τ t)
  (domset (envmap (subst typ ktyp x τ) Γ)) apply scoped_envmap.Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
scoped term ktrm (subst term ktyp x τ t) (domset Γ)
    eapply (scoped_sub_neq term); eauto.Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
ktrm <> ktyp
Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
scoped (SystemF ktyp) ktrm τ (domset Γ)
    +Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
ktrm <> ktyp discriminate.
    +Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
scoped (SystemF ktyp) ktrm τ (domset Γ) unfold scoped.Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
FV (SystemF ktyp) ktrm τ ⊆ domset Γ
      rewrite FV_trm_type_empty.Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
∅ ⊆ domset Γ fsetdec.
  -Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
LC term ktrm (subst term ktyp x τ t) eapply (subst_lc_neq term); auto.Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
ktyp <> ktrm
Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
LC (SystemF ktyp) ktrm τ
    +Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
ktyp <> ktrm discriminate.
    +Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
LC (SystemF ktyp) ktrm τ apply LC_typ_trm.
  -Δ1, Δ2: list (atom * unit)
x: atom
τ: typ LN
Γ: type_ctx
t: term LN
H: scoped term ktyp t (domset (Δ1 ++ x ~ tt ++ Δ2))
H1: scoped typ ktyp τ (domset (Δ1 ++ Δ2))
H2: LC typ ktyp τ
H3: scoped term ktrm t (domset Γ)
H0: LC term ktrm t
H5: LC term ktyp t
LC term ktyp (subst term ktyp x τ t) eapply (subst_lc_eq term); auto.
Qed.

(** ** Structural properties of <<ok_term Δ Γ t>> in <<Γ>> *)
(******************************************************************************)

(** *** Permutation *)
(******************************************************************************)
Lemma ok_term_perm_gamma : forall Δ Γ1 Γ2 t,
    Permutation Γ1 Γ2 ->
    ok_term Δ Γ1 t <->
    ok_term Δ Γ2 t.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN))
  (t : term LN),
Permutation Γ1 Γ2 -> ok_term Δ Γ1 t <-> ok_term Δ Γ2 t
Proof.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN))
  (t : term LN),
Permutation Γ1 Γ2 -> ok_term Δ Γ1 t <-> ok_term Δ Γ2 t
  intros.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
t: term LN
H: Permutation Γ1 Γ2
ok_term Δ Γ1 t <-> ok_term Δ Γ2 t unfold ok_term.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
t: term LN
H: Permutation Γ1 Γ2
scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset Γ1) /\
LC term ktrm t /\ LC term ktyp t <->
scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset Γ2) /\
LC term ktrm t /\ LC term ktyp t
  pose (lemma := scoped_perm_iff term (ktrm : K)).Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
t: term LN
H: Permutation Γ1 Γ2
lemma:= scoped_perm_iff term (ktrm : K): forall (t : term LN) (X : Type)
  (γ1 γ2 : alist X),
Permutation γ1 γ2 ->
scoped term (ktrm : K) t (domset γ1) <->
scoped term (ktrm : K) t (domset γ2)
scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset Γ1) /\
LC term ktrm t /\ LC term ktyp t <->
scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset Γ2) /\
LC term ktrm t /\ LC term ktyp t
  now rewrite lemma; eauto.
Qed.

(** *** Weakening *)
(******************************************************************************)
Lemma ok_term_weak_gamma_r : forall Δ Γ1 Γ2 t,
    ok_term Δ Γ1 t ->
    ok_term Δ (Γ1 ++ Γ2) t.forall (Δ : kind_ctx) (Γ1 : type_ctx)
  (Γ2 : list (atom * typ LN)) (t : term LN),
ok_term Δ Γ1 t -> ok_term Δ (Γ1 ++ Γ2) t
Proof.forall (Δ : kind_ctx) (Γ1 : type_ctx)
  (Γ2 : list (atom * typ LN)) (t : term LN),
ok_term Δ Γ1 t -> ok_term Δ (Γ1 ++ Γ2) t
  unfold ok_term.forall (Δ : kind_ctx) (Γ1 : type_ctx)
  (Γ2 : list (atom * typ LN)) (t : term LN),
scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset Γ1) /\
LC term ktrm t /\ LC term ktyp t ->
scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset (Γ1 ++ Γ2)) /\
LC term ktrm t /\ LC term ktyp t intros.Δ: kind_ctx
Γ1: type_ctx
Γ2: list (atom * typ LN)
t: term LN
H: scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset Γ1) /\
LC term ktrm t /\ LC term ktyp t
scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset (Γ1 ++ Γ2)) /\
LC term ktrm t /\ LC term ktyp t
  intuition (eauto using (scoped_weak_l term)).
Qed.

Lemma ok_term_weak_gamma_l : forall Δ Γ1 Γ2 t,
    ok_term Δ Γ2 t ->
    ok_term Δ (Γ1 ++ Γ2) t.forall (Δ : kind_ctx) (Γ1 : list (atom * typ LN))
  (Γ2 : type_ctx) (t : term LN),
ok_term Δ Γ2 t -> ok_term Δ (Γ1 ++ Γ2) t
Proof.forall (Δ : kind_ctx) (Γ1 : list (atom * typ LN))
  (Γ2 : type_ctx) (t : term LN),
ok_term Δ Γ2 t -> ok_term Δ (Γ1 ++ Γ2) t
  unfold ok_term.forall (Δ : kind_ctx) (Γ1 : list (atom * typ LN))
  (Γ2 : type_ctx) (t : term LN),
scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset Γ2) /\
LC term ktrm t /\ LC term ktyp t ->
scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset (Γ1 ++ Γ2)) /\
LC term ktrm t /\ LC term ktyp t intros.Δ: kind_ctx
Γ1: list (atom * typ LN)
Γ2: type_ctx
t: term LN
H: scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset Γ2) /\
LC term ktrm t /\ LC term ktyp t
scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset (Γ1 ++ Γ2)) /\
LC term ktrm t /\ LC term ktyp t
  intuition (eauto using (scoped_weak_r term)).
Qed.

(** *** Strengthening  *)
(******************************************************************************)
Lemma ok_term_stren_gamma : forall Δ Γ1 Γ2 x τ t,
    ok_term Δ (Γ1 ++ x ~ τ ++ Γ2) t ->
    ~ x `in` (FV term ktrm t) ->
    ok_term Δ (Γ1 ++ Γ2) t.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)) 
  x (τ : typ LN) (t : term LN),
ok_term Δ (Γ1 ++ x ~ τ ++ Γ2) t ->
x `notin` FV term ktrm t -> ok_term Δ (Γ1 ++ Γ2) t
Proof.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)) 
  x (τ : typ LN) (t : term LN),
ok_term Δ (Γ1 ++ x ~ τ ++ Γ2) t ->
x `notin` FV term ktrm t -> ok_term Δ (Γ1 ++ Γ2) t
  introv Hok Hfresh.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
t: term LN
Hok: ok_term Δ (Γ1 ++ x ~ τ ++ Γ2) t
Hfresh: x `notin` FV term ktrm t
ok_term Δ (Γ1 ++ Γ2) t unfold ok_term in *.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
t: term LN
Hok: scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2)) /\
LC term ktrm t /\ LC term ktyp t
Hfresh: x `notin` FV term ktrm t
scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset (Γ1 ++ Γ2)) /\
LC term ktrm t /\ LC term ktyp t
  intuition.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
t: term LN
Hfresh: x `in` FV term ktrm t -> False
H: scoped term ktyp t (domset Δ)
H1: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: LC term ktrm t
H3: LC term ktyp t
scoped term ktrm t (domset (Γ1 ++ Γ2)) eapply (scoped_stren_mid term); eauto.
Qed.

(** *** Substitution *)
(******************************************************************************)
Lemma ok_term_sub_gamma : forall Δ Γ1 Γ2 x τ u t,
    ok_term Δ (Γ1 ++ x ~ τ ++ Γ2) t ->
    ok_term Δ (Γ1 ++ Γ2) u ->
    ok_term Δ (Γ1 ++ Γ2) (subst term ktrm x u t).forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)) 
  x (τ : typ LN) (u t : term LN),
ok_term Δ (Γ1 ++ x ~ τ ++ Γ2) t ->
ok_term Δ (Γ1 ++ Γ2) u ->
ok_term Δ (Γ1 ++ Γ2) (subst term ktrm x u t)
Proof.forall (Δ : kind_ctx) (Γ1 Γ2 : list (atom * typ LN)) 
  x (τ : typ LN) (u t : term LN),
ok_term Δ (Γ1 ++ x ~ τ ++ Γ2) t ->
ok_term Δ (Γ1 ++ Γ2) u ->
ok_term Δ (Γ1 ++ Γ2) (subst term ktrm x u t)
  introv Hokt Hoku.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
Hokt: ok_term Δ (Γ1 ++ x ~ τ ++ Γ2) t
Hoku: ok_term Δ (Γ1 ++ Γ2) u
ok_term Δ (Γ1 ++ Γ2) (subst term ktrm x u t) unfold ok_term, ok_type in *.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
Hokt: scoped term ktyp t (domset Δ) /\
scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2)) /\
LC term ktrm t /\ LC term ktyp t
Hoku: scoped term ktyp u (domset Δ) /\
scoped term ktrm u (domset (Γ1 ++ Γ2)) /\
LC term ktrm u /\ LC term ktyp u
scoped term ktyp (subst term ktrm x u t) (domset Δ) /\
scoped term ktrm (subst term ktrm x u t)
  (domset (Γ1 ++ Γ2)) /\
LC term ktrm (subst term ktrm x u t) /\
LC term ktyp (subst term ktrm x u t)
  intuition.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
scoped term ktyp (subst term ktrm x u t) (domset Δ)
Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
scoped term ktrm (subst term ktrm x u t)
  (domset (Γ1 ++ Γ2))
Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
LC term ktrm (subst term ktrm x u t)
Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
LC term ktyp (subst term ktrm x u t)
  -Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
scoped term ktyp (subst term ktrm x u t) (domset Δ) eapply (scoped_sub_neq term); auto.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
ktyp <> ktrm
    +Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
ktyp <> ktrm discriminate.
  -Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
scoped term ktrm (subst term ktrm x u t)
  (domset (Γ1 ++ Γ2)) eapply (scoped_sub_eq_mid term); eauto.
  -Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
LC term ktrm (subst term ktrm x u t) eapply (subst_lc_eq term); auto.
  -Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
LC term ktyp (subst term ktrm x u t) eapply (subst_lc_neq term); auto.Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
ktrm <> ktyp
    +Δ: kind_ctx
Γ1, Γ2: list (atom * typ LN)
x: atom
τ: typ LN
u, t: term LN
H: scoped term ktyp t (domset Δ)
H1: scoped term ktyp u (domset Δ)
H3: scoped term ktrm t (domset (Γ1 ++ x ~ τ ++ Γ2))
H0: scoped term ktrm u (domset (Γ1 ++ Γ2))
H2: LC term ktrm t
H6: LC term ktyp t
H4: LC term ktrm u
H7: LC term ktyp u
ktrm <> ktyp discriminate.
Qed.


(*
(** ** Example: Typing the polymorphic identity *)
(******************************************************************************)
Example polymorphic_identity_function :
  (nil ; nil ⊢ (Λ λ 0 ⋅ 0) : (∀ 0 ⟹ 0)).
Proof.
  apply j_univ with (L := ∅).
  introv _.
  cbn.
  change (pure (F := fun A => A) ?x) with x.
  apply j_abs with (L := ∅).
  introv _.
  apply j_var.
  - auto with tea_alist.
  - simpl_alist.
    apply ok_tmv_tm_one.
      unfold ok_type, scoped_env, scoped.
      autorewrite with sysf_rw tea_rw_dom.
      split; [fsetdec | apply lc_ty_ty_Fr].
    + simpl_alist. now autorewrite with tea_list.
Qed.

*)