Closed this issue 6 years ago · 1 comments
weaken-synth-expand : ∀{x Γ e τ d Δ τ'} → fresh x d → Γ ⊢ e ⇒ τ ~> d ⊣ Δ → (Γ ,, (x , τ')) ⊢ e ⇒ τ ~> d ⊣ Δ
Turns out to be false! Worked around it.