hazelgrove/hazelnut-dynamics-agda

weaken-synth-expand

Closed this issue · 1 comments

ivoysey commented 
    weaken-synth-expand : ∀{x Γ e τ d Δ τ'} → fresh x d
                                             → Γ ⊢ e ⇒ τ ~> d ⊣ Δ
                                             → (Γ ,, (x , τ')) ⊢ e ⇒ τ ~> d ⊣ Δ
ivoysey commented

Turns out to be false! Worked around it.