¬dCCC(ℕ)
{ ((D 0 THENA Auto) THEN UnfoldTopAb (-1)) }
1. ∀R:ℕ ⟶ ℕ ⟶ 𝔹. ((∀g:ℕ ⟶ ℕ. ∃n:ℕ. (↑(R n (g n)))) 
⇒ (∃n:ℕ. ∀m:ℕ. (↑(R n m))))
⊢ False