structure CC.Rebind {s1 s2 : Sig} (env1 : TypeEnv s1) (f : Rename s1 s2) (env2 : TypeEnv s2) : Prop

• var {k : Kind} (x : BVar s1 k) : env1.lookup x = env2.lookup (f.var x)

def CC.Rebind.liftVar {a✝ : Sig} {env1 : TypeEnv a✝} {s2✝ : Sig} {f : Rename a✝ s2✝} {env2 : TypeEnv s2✝} {x : ℕ} (ρ : Rebind env1 f env2) : Rebind (env1.extend_var x) f.lift (env2.extend_var x)

Equations

• ⋯ = ⋯

def CC.Rebind.liftTVar {a✝ : Sig} {env1 : TypeEnv a✝} {s2✝ : Sig} {f : Rename a✝ s2✝} {env2 : TypeEnv s2✝} {d : PreDenot} (ρ : Rebind env1 f env2) : Rebind (env1.extend_tvar d) f.lift (env2.extend_tvar d)

Equations

• ⋯ = ⋯

def CC.Rebind.liftCVar {a✝ : Sig} {env1 : TypeEnv a✝} {s2✝ : Sig} {f : Rename a✝ s2✝} {env2 : TypeEnv s2✝} (ρ : Rebind env1 f env2) (cs : CaptureSet ∅) : Rebind (env1.extend_cvar cs) f.lift (env2.extend_cvar cs)

Equations

• ⋯ = ⋯

theorem CC.rebind_resolved_capture_set {s1 : Sig} {env1 : TypeEnv s1} {s2✝ : Sig} {f : Rename s1 s2✝} {env2 : TypeEnv s2✝} {C : CaptureSet s1} (ρ : Rebind env1 f env2) : C.subst (Subst.from_TypeEnv env1) = (C.rename f).subst (Subst.from_TypeEnv env2)

theorem CC.rebind_captureset_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {f : Rename s1 s2} {env2 : TypeEnv s2} (ρ : Rebind env1 f env2) (C : CaptureSet s1) : CaptureSet.denot env1 C = CaptureSet.denot env2 (C.rename f)

theorem CC.rebind_capturebound_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {f : Rename s1 s2} {env2 : TypeEnv s2} (ρ : Rebind env1 f env2) (B : CaptureBound s1) : CaptureBound.denot env1 B = CaptureBound.denot env2 (B.rename f)

@[irreducible]

def CC.rebind_shape_val_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {f : Rename s1 s2} {env2 : TypeEnv s2} (ρ : Rebind env1 f env2) (T : Ty TySort.shape s1) : Ty.shape_val_denot env1 T ≈ Ty.shape_val_denot env2 (T.rename f)

Equations

• ⋯ = ⋯

@[irreducible]

def CC.rebind_capt_val_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {f : Rename s1 s2} {env2 : TypeEnv s2} (ρ : Rebind env1 f env2) (T : Ty TySort.capt s1) : Ty.capt_val_denot env1 T ≈ Ty.capt_val_denot env2 (T.rename f)

Equations

• ⋯ = ⋯

@[irreducible]

def CC.rebind_exi_val_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {f : Rename s1 s2} {env2 : TypeEnv s2} (ρ : Rebind env1 f env2) (T : Ty TySort.exi s1) : Ty.exi_val_denot env1 T ≈ Ty.exi_val_denot env2 (T.rename f)

Equations

• ⋯ = ⋯

def CC.rebind_capt_exp_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {f : Rename s1 s2} {env2 : TypeEnv s2} (ρ : Rebind env1 f env2) (T : Ty TySort.capt s1) : Ty.capt_exp_denot env1 T ≈ Ty.capt_exp_denot env2 (T.rename f)

Equations

• ⋯ = ⋯

@[irreducible]

def CC.rebind_exi_exp_denot {s1 s2 : Sig} {env1 : TypeEnv s1} {f : Rename s1 s2} {env2 : TypeEnv s2} (ρ : Rebind env1 f env2) (T : Ty TySort.exi s1) : Ty.exi_exp_denot env1 T ≈ Ty.exi_exp_denot env2 (T.rename f)

Equations

• ⋯ = ⋯

def CC.Rebind.weaken {s : Sig} {env : TypeEnv s} {x : ℕ} : Rebind env Rename.succ (env.extend_var x)

Equations

• ⋯ = ⋯

def CC.Rebind.tweaken {s : Sig} {env : TypeEnv s} {d : PreDenot} : Rebind env Rename.succ (env.extend_tvar d)

Equations

• ⋯ = ⋯

def CC.Rebind.cweaken {s : Sig} {env : TypeEnv s} {cs : CaptureSet ∅} : Rebind env Rename.succ (env.extend_cvar cs)

Equations

• ⋯ = ⋯

theorem CC.weaken_shape_val_denot {s : Sig} {x : ℕ} {env : TypeEnv s} {T : Ty TySort.shape s} : Ty.shape_val_denot env T ≈ Ty.shape_val_denot (env.extend_var x) (T.rename Rename.succ)

theorem CC.weaken_capt_val_denot {s : Sig} {x : ℕ} {env : TypeEnv s} {T : Ty TySort.capt s} : Ty.capt_val_denot env T ≈ Ty.capt_val_denot (env.extend_var x) (T.rename Rename.succ)

theorem CC.weaken_exi_val_denot {s : Sig} {x : ℕ} {env : TypeEnv s} {T : Ty TySort.exi s} : Ty.exi_val_denot env T ≈ Ty.exi_val_denot (env.extend_var x) (T.rename Rename.succ)

theorem CC.tweaken_shape_val_denot {s : Sig} {d : PreDenot} {env : TypeEnv s} {T : Ty TySort.shape s} : Ty.shape_val_denot env T ≈ Ty.shape_val_denot (env.extend_tvar d) (T.rename Rename.succ)

theorem CC.tweaken_capt_val_denot {s : Sig} {d : PreDenot} {env : TypeEnv s} {T : Ty TySort.capt s} : Ty.capt_val_denot env T ≈ Ty.capt_val_denot (env.extend_tvar d) (T.rename Rename.succ)

theorem CC.tweaken_exi_val_denot {s : Sig} {d : PreDenot} {env : TypeEnv s} {T : Ty TySort.exi s} : Ty.exi_val_denot env T ≈ Ty.exi_val_denot (env.extend_tvar d) (T.rename Rename.succ)

theorem CC.cweaken_shape_val_denot {s : Sig} {env : TypeEnv s} {cs : CaptureSet ∅} {T : Ty TySort.shape s} : Ty.shape_val_denot env T ≈ Ty.shape_val_denot (env.extend_cvar cs) (T.rename Rename.succ)

theorem CC.cweaken_capt_val_denot {s : Sig} {env : TypeEnv s} {cs : CaptureSet ∅} {T : Ty TySort.capt s} : Ty.capt_val_denot env T ≈ Ty.capt_val_denot (env.extend_cvar cs) (T.rename Rename.succ)

theorem CC.cweaken_exi_val_denot {s : Sig} {env : TypeEnv s} {cs : CaptureSet ∅} {T : Ty TySort.exi s} : Ty.exi_val_denot env T ≈ Ty.exi_val_denot (env.extend_cvar cs) (T.rename Rename.succ)