Library Lambda.CCSum.Thinning


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.CCSum.Types.

Require
 Import
 Lambda.CCSum.Inversion.




Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

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




  Inductive
 ins_in_env A
 : nat → env → env → Prop
 :=

    | ins_O : ∀ e
, ins_in_env A
 0 e
 (A
 :: e
)

    | ins_S :

        ∀ n
 e
 f
 t
,

        ins_in_env A
 n
 e
 f
 →

        ins_in_env A
 (S n
) (t
 :: e
) (lift_rec 1 t
 n
 :: f
).




  Hint
 Resolve
 ins_O ins_S: coc
.




  Lemma
 ins_item_ge :

   ∀ A
 n
 e
 f
,

   ins_in_env A
 n
 e
 f
 →

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




  Lemma
 ins_item_lt :

   ∀ A
 n
 e
 f
,

   ins_in_env A
 n
 e
 f
 →

   ∀ v
 : nat,

   n
 > v
 → ∀ t
, item_lift t
 e
 v
 → item_lift (lift_rec 1 t
 n
) f
 v
.




  Lemma
 typ_weak_weak :

   ∀ A
 e
 t
 T
,

   typ e
 t
 T
 →

   ∀ n
 f
,

   ins_in_env A
 n
 e
 f
 → wf
 f
 → typ f
 (lift_rec 1 t
 n
) (lift_rec 1 T
 n
).




  Theorem
 thinning :

   ∀ e
 t
 T
,

   typ e
 t
 T
 → ∀ A
, wf
 (A
 :: e
) → typ (A
 :: e
) (lift 1 t
) (lift 1 T
).




  Lemma
 thinning_n :

   ∀ n
 e
 f
,

   trunc _
 n
 e
 f
 →

   ∀ t
 T
, typ f
 t
 T
 → wf
 e
 → typ e
 (lift n
 t
) (lift n
 T
).