jonaprieto/agda-prop

Proofs for spliting auxiliar theorems for agda-metis

jonaprieto opened this issue · 0 comments

jonaprieto commented

In Negation module of Theorems folder, I postulated:

postulate
  ¬⇔-to-⇒¬∧⇒¬
    : ∀ {Γ} {φ₁ φ₂}
    → Γ ⊢ ¬ (φ₁ ⇔ φ₂)
    → Γ ⊢ (φ₁ ⇒ φ₂) ∧ (φ₂ ⇒ ¬ φ₁)

We need the proof because is used in agda-metis to split goals see jonaprieto/agda-metis#9.