From 34385c4f1ac2e6fb4ee2606b269bd9d62b4b743d Mon Sep 17 00:00:00 2001
From: tomaz1502 <tomgm1502@gmail.com>
Date: Tue, 24 Oct 2023 17:29:07 -0300
Subject: [PATCH] clean up

---
 Smt/Tactic/Cvc5Proof.lean | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/Smt/Tactic/Cvc5Proof.lean b/Smt/Tactic/Cvc5Proof.lean
index 16522374..f066df16 100644
--- a/Smt/Tactic/Cvc5Proof.lean
+++ b/Smt/Tactic/Cvc5Proof.lean
@@ -135,11 +135,6 @@ def cvc5Proof4: Cvc5Proof := {
   lastName := `pf
 }
 
-example (P Q : Prop) : Q → ¬ P ∨ Q := by
-  intro lean_a0
-  have lean_a1: ¬ P ∨ Q := scope (fun hp => lean_a0)
-  exact lean_a1
-
 def cvc5Proof5: Cvc5Proof := {
   steps := [ .intro `lean_a0
            , .scope `lean_a1 "P" "Q" `hp `inner_pf 
@@ -176,6 +171,3 @@ example (P Q : Prop) : Not (P → ((P → Q) → Q)) → False := by
 example (P Q : Prop) : Q → ¬ P ∨ Q := by
   test 5
 
-  /- intro lean_a0 -/
-  /- have lean_a1: ¬ P ∨ Q := scope (fun hp => lean_a0) -/
-  /- exact lean_a1 -/