jonaprieto/agda-prop

Provide a proof

jonaprieto opened this issue · 0 comments

New in the Implication module but without a proof.

postulate
  ⇒∧⇒-to-⇒∧
    : ∀ {Γ} {φ ψ γ}
    → Γ ⊢ (φ ⇒ ψ) ∧ (φ ⇒ γ)
    → Γ ⊢ φ ⇒ (ψ ∧ γ)

@camilorodriguezga Would you like to contribute with the proof of this theorem? 👍

In 60ea090