Open hferee opened 4 months ago
A lazy implementation of the implication could simplify⊤→ φ into φ.
However, the soundness of this implication seems to require the following lemma:
Lemma ImpLImp_swap Γ φ1 φ2 φ3 θ: Γ • (φ1 → φ2 → φ3) ⊢ θ -> Γ • (φ2 → φ1 → φ3)⊢ θ.
A lazy implementation of the implication could simplify⊤→ φ into φ.
However, the soundness of this implication seems to require the following lemma: