From 4c23040dfadd6e5ef1a46f8ed8db4cb231ec4edc Mon Sep 17 00:00:00 2001
From: Mroik <mroik@delayed.space>
Date: Thu, 25 Jul 2024 02:40:50 +0200
Subject: [PATCH] Add subproof level check for iff

---
 src/app.rs   | 4 +---
 src/fitch.rs | 6 ++++++
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/app.rs b/src/app.rs
index 7064025..d7c5b58 100644
--- a/src/app.rs
+++ b/src/app.rs
@@ -48,9 +48,7 @@ impl App {
             | State::OrState(OrState::EliminateGetAssumption) => {
                 ("And expression to eliminate", true)
             }
-            State::AndState(AndState::EliminateGetProposition(_)) => {
-                ("Resulting expression", true)
-            }
+            State::AndState(AndState::EliminateGetProposition(_)) => ("Resulting expression", true),
             State::OrState(OrState::EliminateGetLeftSubproof(_))
             | State::OrState(OrState::EliminateGetRightSubproof(_, _))
             | State::ImpliesState(ImpliesState::Introduce)
diff --git a/src/fitch.rs b/src/fitch.rs
index 745d38c..ee7b009 100644
--- a/src/fitch.rs
+++ b/src/fitch.rs
@@ -556,6 +556,12 @@ impl Fitch {
             Some(v) => v,
         };
 
+        if self.current_level != self.statements.get(left_sub).unwrap().0 - 1
+            || self.current_level != self.statements.get(right_sub).unwrap().0 - 1
+        {
+            return false;
+        }
+
         if !(left_start == right_end && left_end == right_start) {
             return false;
         }