qed on failed subproof

contradiction_proof.py

@@ -23,4 +23,5 @@
 p.switchSidesOfEqual(8)
 p.notElim(6,9)
 p.concludeSubproof(6)
-#p.impliesIntroduction([4,5],11)
+p.impliesIntroduction([4,5],11)
+p.qed(12)

logicObjects.py

@@ -70,6 +70,17 @@ def elim(self, arg):
         if arg==self.assum:
             return self.conc
 
+    def __eq__(self, other):
+        return self.assum == other.assum and self.conc == other.conc
+
+    def __repr__(self):
+        assumptionstr = ""
+        for assumption in self.assum:
+            assumptionstr += str(assumption)
+            assumptionstr += ", "
+        assumptionstr = assumptionstr[:-2]
+        return  assumptionstr + " → " +  str(self.conc)
+
 class Not:
     def __init__(self, arg):
         self.arg = arg

proof.py

@@ -615,4 +615,17 @@ def notElim(self, lineNum1, lineNum2):
             self.justifications += [f'Contradiction from lines {lineNum1} and {lineNum2}']
             self.show()
         else:
-            print(f"The statement on line {lineNum1} isn't a Not")
+            print(f"The statement on line {lineNum1} isn't a Not")
+
+    def impliesIntroduction(self, lineNumsAssums, lineNumConc): # needs work, a lot of it
+        '''
+        Introduce an implication based on assumptions and a conclusion
+        :param lineNumsAssums: the lines containing the assumptions
+        :param lineNumConc: the line to conclude
+        '''
+        assums = []
+        for line in lineNumsAssums:
+            assums.append(self.steps[line])
+        self.steps += [Implies(assums,self.steps[lineNumConc])]
+        self.justifications += [f"Introduced implies based on assumptions on lines {lineNumsAssums} to conclude line {lineNumConc}"]
+        self.show()