∀n:ℕ. Dec(reducible(n))
{ (Assert ⌜∀n:ℕ. Dec((n = 0 ∈ ℤ) ∨ reducible(n))⌝⋅ THEN Auto) }
.....decidable?.....
1. n : ℕ
⊢ Dec((n = 0 ∈ ℤ) ∨ reducible(n))
1. ∀n:ℕ. Dec((n = 0 ∈ ℤ) ∨ reducible(n))
2. n : ℕ
⊢ Dec(reducible(n))