draining

source/math.mmt

@@ -307,7 +307,7 @@ theory Sequences =
 	include ?Logic ❙
 	
 	forall_seq : {A: type}{n} (A^n ⟶ prop) ⟶ prop ❘ # ∀n 3 prec -101 ❙
-	exists_seq : {A: type}{n} (A^n ⟶ prop) ⟶ prop ❘ # ∃n 3 prec -101 ❘ = [A,n][P] ¬ forall_seq A n [s : A^n] ¬ (P s)❙
+	exists_seq : {A: type}{n} (A^n ⟶ prop) ⟶ prop ❘ # ∃n 3 prec -101 ❘ ¬ (P s = [A,n][P] ¬ forall_seq A n [s : A^n])❙
 ❚
 
 theory Math : ur:?PLF =