Fix broken or elimination

source/math.mmt

@@ -97,13 +97,12 @@ theory NaturalDeduction : ur:?LF =
      equiv_introduction : {A,B} ⊦ (A ⇒ B) ⟶ ⊦ (B ⇒ A) ⟶ ⊦ (A ⇔ B) ❘ # equivi 3 4❙
      biimplication_elimination_left : {A, B}⊦ (A ⇔ B) ⟶ ⊦ (A ⇒ B) ❘ # biell 3❙
      biimplication_elimination_right : {A,B}⊦ (A ⇔ B) ⟶ ⊦ (B ⇒ A) ❘ # bielr 3❙
-     or_elimination : {A,B,C} ⊦ (A ∨ B) ⟶ (⊦ A ⟶ ⊦ C) ⟶ (⊦ B ⟶ ⊦ C) ⟶ ⊦ C ❘ # orelim 3 4 5❙
-     modus_ponens : {A,B} (⊦ A ⇒ B) ⟶ ⊦ A ⟶ ⊦ B ❘ # MP 3 4 ❙
+     or_elimination : {A,B,C} ⊦ (A ∨ B) ⟶ (⊦ A ⟶ ⊦ C) ⟶ (⊦ B ⟶ ⊦ C) ⟶ ⊦ C ❘ # orelim 4 5 6❙
+     modus_ponens : {A,B} (⊦ A ⇒ B) ⟶ ⊦ A ⟶ ⊦ B ❘# MP 3 4 ❙
 	 /T basic axioms governing Equality. Again, all the type parameters can be left implicit ❙
 	 eq_refl : {t:𝒰 100,A: t} ⊦ A ≐ A ❘ # eq_refl 2❙
 	 eq_cong : {t : 𝒰 100, s : 𝒰 100, f : t ⟶ s, A : t, B: t}
 	 		⊦ A ≐ B ⟶ ⊦ (f A) ≐ (f B) ❘ # eq_cong 3 6❙
-     // biimplication_elimination_left : {A,B}⊦ (A ⇔ B) ⟶ ⊦ (A ⇒ B) ❘ # biell 3 ❙
 ❚