Library Lambda.CCSum.Substitution


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.CCSum.Types.

Require
 Import
 Lambda.CCSum.Inversion.

Require
 Import
 Lambda.CCSum.Thinning.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

Implicit
 Types
 A
 B
 M
 N
 T
 t
 u
 v
 : term.




  Lemma
 wf_sort_lift :

   ∀ n
 e
 t
, wf
 e
 → item_lift t
 e
 n
 → ∃ s
 : sort, typ e
 t
 (Srt s
).




  Inductive
 sub_in_env t
 T
 : nat → env → env → Prop
 :=

    | sub_O : ∀ e
, sub_in_env t
 T
 0 (T
 :: e
) e


    | sub_S :

        ∀ e
 f
 n
 u
,

        sub_in_env t
 T
 n
 e
 f
 →

        sub_in_env t
 T
 (S n
) (u
 :: e
) (subst_rec t
 u
 n
 :: f
).




  Hint
 Resolve
 sub_O sub_S: coc
.




  Lemma
 nth_sub_sup :

   ∀ t
 T
 n
 e
 f
,

   sub_in_env t
 T
 n
 e
 f
 →

   ∀ v
 : nat, n
 ≤ v
 → ∀ u
, item _
 u
 e
 (S v
) → item _
 u
 f
 v
.




  Lemma
 nth_sub_eq : ∀ t
 T
 n
 e
 f
, sub_in_env t
 T
 n
 e
 f
 → item _
 T
 e
 n
.




  Lemma
 nth_sub_inf :

   ∀ t
 T
 n
 e
 f
,

   sub_in_env t
 T
 n
 e
 f
 →

   ∀ v
 : nat,

   n
 > v
 → ∀ u
, item_lift u
 e
 v
 → item_lift (subst_rec t
 u
 n
) f
 v
.




  Lemma
 typ_sub_weak :

   ∀ g
 (d
 : term) t
,

   typ g
 d
 t
 →

   ∀ e
 u
 (U
 : term),

   typ e
 u
 U
 →

   ∀ f
 n
,

   sub_in_env d
 t
 n
 e
 f
 →

   wf
 f
 → trunc _
 n
 f
 g
 → typ f
 (subst_rec d
 u
 n
) (subst_rec d
 U
 n
).




  Theorem
 substitution :

   ∀ e
 t
 u
 (U
 : term),

   typ (t
 :: e
) u
 U
 →

   ∀ d
 : term, typ e
 d
 t
 → typ e
 (subst d
 u
) (subst d
 U
).