Closed this issue 6 years ago · 1 comments
need to figure out how to do substitution (value substitution only?) and prove the substitution lemma(s)
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 :: τ