hazelgrove/hazelnut-dynamics-agda

prove substitution lemmas

Closed this issue · 1 comments

cyrus- commented

need to figure out how to do substitution (value substitution only?) and prove the substitution lemma(s)

ivoysey commented

so far, this is the one i think i'll need

  lem-subst : ∀{Δ Γ x τ1 d1 τ d2 } →
              Δ , Γ ,, (x , τ1) ⊢ d1 :: τ →
              Δ , Γ ⊢ d2 :: τ1 →
              Δ , Γ ⊢ [ d2 / x ] d1 :: τ