Mcltt.Core.Soundness.Weakening.Definitions

From Mcltt.Core Require Import Base.
From Mcltt.Core.Syntactic Require Export SystemOpt.
Import Syntax_Notations.

Generalizable All Variables.

Reserved Notation "Γ ⊢w σ : Δ" (in custom judg at level 80, Γ custom exp, σ custom exp, Δ custom exp).

Inductive weakening : ctx -> sub -> ctx -> Prop :=
| wk_id :
  `( {{ Γ s σ Id : Δ }} ->
     {{ Γ w σ : Δ }} )
| wk_p :
  `( {{ Γ w τ : Δ', A }} ->
     {{ Δ' Δ }} ->
     {{ Γ s σ Wk τ : Δ }} ->
     {{ Γ w σ : Δ }} )
where "Γ ⊢w σ : Δ" := (weakening Γ σ Δ) (in custom judg) : type_scope.

#[export]
 Hint Constructors weakening : mcltt.