Theorem: Smt.Reconstruct.Prop.cnfEquivPos1 (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
⊢ ∀ {p q : Prop}, p ≠ q ∨ ¬p ∨ q
Tactic:
intros _ _
State after:
p✝ q✝ : Prop
⊢ p✝ ≠ q✝ ∨ ¬p✝ ∨ q✝

State before:
p✝ q✝ : Prop
⊢ p✝ ≠ q✝ ∨ ¬p✝ ∨ q✝
Tactic:
apply orImplies
State after:
case a
p✝ q✝ : Prop
⊢ ¬p✝ ≠ q✝ → ¬p✝ ∨ q✝

State before:
case a
p✝ q✝ : Prop
⊢ ¬p✝ ≠ q✝ → ¬p✝ ∨ q✝
Tactic:
exact equivElim1 ∘ notNotElim
State after:
no goals