ivoysey opened this issue 6 years ago · 0 comments
expand-ana-disjoint : ∀{ e1 e2 τ1 τ2 e1' e2' τ1' τ2' Γ Δ1 Δ2 } → holes-disjoint e1 e2 → Γ ⊢ e1 ⇐ τ1 ~> e1' :: τ1' ⊣ Δ1 → Γ ⊢ e2 ⇐ τ2 ~> e2' :: τ2' ⊣ Δ2 → Δ1 ## Δ2