<p>Let us spell out the informal meaning of <code>INat</code>, <code>IntNat</code> and <code>IndNat2</code>. Suppose we have a predicate <code>P</code> on natural numbers. Say that <code>P</code> is <em>inductive</em> if we can inhabit <code>P Zero</code> and <code>∀ k . P k -&gt; P (Succ k)</code>. Then we have:</p>

<ul>
<li><code>NatInd P</code> states "if <code>P</code> is inductive then, for all <code>j : Nat</code>, we have <code>P j</code>"</li>
<li><code>INat n P</code> states "if <code>P</code> is inductive then <code>P n</code>"</li>
<li><code>NatInd2 P</code> states: "if <code>P</code> is inductive and for every <code>n</code> we have an <code>i</code> which allows us to inhabit inductive predicates at <code>n</code>, then we can inhabit <code>P n</code>".</li>
</ul>

<p>As you can see, <code>NatInd2</code> just sweeps the problem under the rug, because it essentially asks that we give it a way of implementing induction. It is true that we can inhabit <code>INat Zero</code>, <code>INat (Succ Zero)</code>, <code>INat (Succ (Succ Zero))</code>, ... but that does <em>not</em> imply that we can inhabit <code>∀ k . INat k</code>! If you think otherwise, provide a term that does so.</p>

<p>In essence, you just hid the problem a little deeper by introducing a level of indirection. You could have already asked this: I can inhabit an infinite sequence of types <code>NatInd P S Z Zero</code>, <code>NatInd P S Z (Succ Zero)</code>, <code>NatInt P S Z (Succ (Succ Zero))</code>, ... – why is this not sufficient to have induction? The answer: because you are suposed to inhabit <code>∀ n : Nat, NatInd P S Z n</code>, which is <em>not</em> the same thing! The former is <em>truth</em> at the meta-level and the latter is an <em>internal induction principle</em> inside the calculus.</p>

<p>The question revolves around the difference between having an infinite sequence of terms inhabiting</p>

<pre><code>t0 : Q 0
t1 : Q 1
t2 : Q 2
t3 : Q 3
...
</code></pre>

<p>versus having a single term</p>

<pre><code>t : ∀ n : Nat, Q n
</code></pre>

<p>Given <code>t</code>, we can of course produce <code>t0</code>, <code>t1</code>, <code>t2</code>, etc. But there is generally no way to produce a <code>t</code> if we know that we have the infinite sequence of terms <code>t0</code>, <code>t1</code>, <code>t2</code>, ..., <em>even in the case</em> when there is an algorithm generating the sequence, for such an algorithm may not be expressible in the language (CiC in our case). Is that clear?</p>

<p>In fact, we can show that, given <em>any</em> (sufficiently expressive) strongly normalizing calculus (and a total language in general), there will be an instance of <code>Q : Nat -&gt; *</code> such that we can inhabit each of <code>Q 0</code>, <code>Q 1</code>, <code>Q 2</code>, ... separately, but not <code>∀ n : Nat, Q n</code>. This just says that no strongly normalizing calculus can express all total computable functions.</p>

<p><strong>Supplemental:</strong> The OP is aksing <em>why</em> one needs, ought, or should internalize universal quantifiers. From a programmer's point of view the answer is simply that this is what is needed. Let us consider the practical difference between having an infinite sequence of terms</p>

<pre><code>t0 : P 0
t1 : P 1
t2 : P 2
...
</code></pre>

<p>versus a single term</p>

<pre><code>u : ∀ n : Nat, P n
</code></pre>

<p>Suppose you want to write a program which reads from the standard input a natural number <code>k</code> and outputs a witness of the statement <code>P k</code>. If we have <code>u</code> then we can do it easily (I am inventing syntax as I go here):</p>

<pre><code>print "Please enter a natural number" ;
let k = input() in
print (u k)
</code></pre>

<p>How could we write such a program if instead of <code>u</code> we had a sequence of terms <code>t0</code>, <code>t1</code>, <code>t2</code>, as above? One could attempt something like</p>

<pre><code>print "Please enter a natural number" ;
let k = input() in
if k = 0 then print t0
else if k = 1 then print t1
else if k = 2 then print t2
...
</code></pre>

<p>but this will not do because programs cannot be infinite. One could also try to do it as follows, assuming there is an algorithm <code>A</code> which produces the sequence <code>t0</code>, <code>t1</code>, <code>t2</code> (but this algorithm is not expressible in our programming language):</p>

<ol>
<li>The programmer asks the user to tell him a natural number.</li>
<li>The user provides a natural number <code>k</code>.</li>
<li>The programer runs <code>A</code> to get the expression <code>tk</code> of type <code>P k</code>.</li>
<li>The programer writes down the program <code>print (u tk)</code> and runs it.</li>
</ol>

<p>We can see quite plainly that the programmer is now doing the job of the program, i.e., everything has moved to the meta-level, which is <em>not</em> what we want. We want the machines to do the job for us. You could also use a programming language which <em>can</em> express the algorithm <code>A</code>, but then you've switched to a different programming language and your algorithm <code>A</code> will correspond to the original program <code>u</code>.</p>

<p>The program <code>u</code> is needed because we must be able to <em>compose</em> and <em>combine</em> it with other pieces of code where it is <em>not</em> known in advance how <code>u</code> will be used.</p>

<p>We can also take the logical point of view. What is the difference between having at our disposal an infinite sequence of proofs</p>

<pre><code>t0 : P 0
t1 : P 1
t2 : P 2
...
</code></pre>

<p>versus a single proof</p>

<pre><code>u : ∀ n : Nat, P n
</code></pre>

<p>When we inspect <code>u</code> and verify that it is valid, we have provided evidence that <code>P</code> holds for all numbers. In contrast, the sequence of proofs <code>t0</code>, <code>t1</code>, <code>t2</code>, ... is <em>not</em> a finite amount of information, and so it cannot be verified and validated in finite time. Such infinite amount of information does not provide evidence that <code>P</code> holds for all numbers, at least not according to the standard that <em>evidence</em> in mathematics means <em>proof</em>. A proof by definition is finite and verifiable.</p>

<p>You may try to save the day by saying something like "but if we verify the algorithm that produces the sequence <code>t0</code>, <code>t1</code>, <code>t2</code>, ... then we will know that <code>P</code> holds for all <code>n</code>". This is true, but again, you're switching to the meta-level in which the verification that the algorithm works corresponds to having the proof <code>u</code>.</p>

CC BY-SA 4.0
2018-08-14T13:21:04.977Z
I'm very sorry but I don't think that covers my doubt. I understand *"that does not imply that we can inhabit ∀ k . INat k"* but don't understand **why you should**, nor why *"you are suposed to inhabit ∀ n : Nat, NatInd P S Z n"*. I understand that there is not an algorithm on the language capable of producing `t0`, `t1`, `t2` given a `n : Nat`, but I don't understand **why, in practice, you need that**. What I see is that, anytime you'd use `NatInd`, you need a `n : Nat` to get a result. Anytime you'd use `NatInt2`, you need a `n : Nat` and `i : INat n`. So, what (...)
MaiaVictor
CC BY-SA 4.0
2018-08-14T13:25:28.537Z
(...) I'm having trouble is figuring out "when", or "in what practical situation" `NatInt2` wouldn't be enough, because, in the context of "programming", anytime you can provide a `n` to `NatInt`, the programmer could just provide a pair `n, i` to `NatInt2` and get the same result. Similarly, if we take CoC as a formalization of mathematics, a proof of `∀ n : Nat . ∀ i : INat n . P n` would clearly imply that `P` truly holds for all `n` - which is what we want, right? So, in the context of proving mathematical theorems, I, too, I don't understand when `NatInt2` wouldn't suffice.
MaiaVictor
CC BY-SA 4.0
2018-08-14T13:26:17.083Z
(I meant NatInd not NatInt. And sorry for making those additional comments, but I think I should be honest when I don't understand a point, despite being given a great explanation.)
MaiaVictor
CC BY-SA 4.0
2018-08-14T13:33:45.997Z
Btw, `∀ n : Nat . ∀ i : INat n . P n` implies `∀ n : Nat . P n` because we can construct a `INat n` for all `n`, even though we can't do that inside the language (i.e., there is no proof of `∀ n : Nat -> INat n`). So, perhaps the issue is that it is somehow it is considered essential to have that last bit internalized, but what I don't get is, "why"? Again, for programming, the editor could just fill the `INat n`. For mathematics, anyone reading `∀ n : Nat . ∀ i : INat n . P n` would be equally convinced that `P n` holds for all `n`. Right?
MaiaVictor
CC BY-SA 4.0
2018-08-14T20:27:34.297Z
It is false that `∀ n : Nat . ∀ i : INat n . P n` implies `∀ n : Nat . P n`. For that to be the case, you need to provide a term of type `(∀ n : Nat . ∀ i : INat n . P n) → ∀ n : Nat . P n`, which you cannot do. What you are observing is that *every instance* can be inahbited, which is useless from a programming point of view. I supplemented my answer with an explanation of why this is so.
Andrej Bauer
CC BY-SA 4.0
2018-08-14T20:56:26.293Z
The example made it obvious. Sorry for not getting it before.
MaiaVictor
CC BY-SA 4.0
2018-08-14T09:18:32.933Z
2018-08-14T20:52:43.053Z
2018-08-14T20:52:43.053Z
Andrej Bauer
<p>It is well known that it is impossible to prove the induction principle for Natural numbers on the Calculus of Constructions. That is,</p>

<pre><code>Nat =
  ∀ P : *
  ∀ S : P -&gt; P
  ∀ Z : P
  P

Zero =
  λ P : *
  λ S : P -&gt; P
  λ Z : P
  Z

Succ =
  λ n : Nat
  λ P : *
  λ S : P -&gt; P
  λ Z : P
  S (n P S Z)

NatInd :
  ∀ P : Nat -&gt; *
  ∀ S : ∀ (n : Nat) -&gt; P n -&gt; P (Succ n)
  ∀ Z : P Zero
  ∀ n : Nat
  P n
</code></pre>

<p>There is no term of type <code>NatInd</code> on CoC, for either this or any other representation of <code>Nat</code>. But I've noticed that the following slightly different type can be constructed:</p>

<pre><code>INat =
  λ n : Nat
  ∀ P : Nat -&gt; *
  ∀ S : ∀ (n : Nat) -&gt; P n -&gt; P (S n)
  ∀ Z : P Zero
  P n

NatInd2 :
  ∀ P : Nat -&gt; *
  ∀ S : ∀ (n : Nat) -&gt; P n -&gt; P (Succ n)
  ∀ Z : P Zero
  ∀ n : Nat
  ∀ i : INat n
  P n
</code></pre>

<p>Here, we first define a new type, <code>INat : Nat -&gt; *</code>. That type is isomorphic to Nats and can be easily constructed for any natural number. Then, <code>NatInd2</code> is a term that, given a proposition indexed on Nats, a base case <code>Z</code>, a step case <code>S</code>, for any nat <code>n</code> and its corresponding <code>INat n</code>, proves <code>P(n)</code> holds for every <code>n</code>. Or, in simpler words, <code>NatInd2</code> is essentially induction, except that you must provide an additional argument <code>i</code> of type <code>INat n</code>, which you can always construct anyway. You could as well use dependent pairs to conveniently store <code>Nat, INat</code> pairs together.</p>

<p>It seems like this accomplishes the same one would expect from induction, i.e., you prove all cases from a base and a step case. Of course, there is an extra argument, but that argument is trivial to construct. For a "human reader", any proof using the method above would be equally convincing that some property holds for all <code>n</code>. So, my question is: <strong>is there any reason for the above method to be insufficient in general? Why is it so important to have the former unaltered definition of <code>NatInd</code>?</strong></p>

CC BY-SA 4.0
2018-08-09T13:19:03.363Z
You have the type Nat which only has recursion, but not induction (i.e. the type of the result can't depend on the input). Then you build Nat2 (named INat) which allows you to have some kind of weak induction: if you give a Nat2 as input, then the type of the output can depend on a Nat.
xavierm02
CC BY-SA 4.0
2018-08-09T13:25:39.447Z
@xavierm02 yes, I think that's more or less what I did. My question is pretty much "why that is not enough", perhaps in a philosophical sense? Because as I understand, an inductive proof using `NatInd2` would be equally "truthful" as an inductive proof using `NatInt`.
MaiaVictor
CC BY-SA 4.0
2018-08-09T13:30:19.853Z
My intuition is that:
(1) You will need to define Nat3, Nat4 etc. to do some things. (2) There may be (very weird convoluted?) things for which no Natn would work. (3) You may be interested in the trick to get induction from recursion plus induction for the equality type.
xavierm02
CC BY-SA 4.0
2018-08-09T14:05:06.283Z
I'm not even convinced you can build an element of INat / Nat2.
xavierm02
CC BY-SA 4.0
2018-08-09T15:50:38.730Z
@xavierm02 [here](https://gist.github.com/MaiaVictor/35b60441237510a0161450e278f952c8) is a construction of that INat. About (1), I think that is ok, can even be added automatically. About (2), maybe. About (3), do you have a name / reference for that trick?
MaiaVictor
CC BY-SA 4.0
2018-08-09T17:24:21.767Z
The trick was something like this:
(1) Change the domain to $\Sigma_{n:\mathbb N}P n$ to make it non-dependent.
(2) Use the recursion principle to build a term $t$ of type $\forall P : \mathbb N \to Type, \forall z : P Z, \forall s : (\forall n : \mathbb N, P n \to P (S n)), \forall n, \Sigma_{n:\mathbb N}P n$
(3) Define the induction principle as the first projection of the previous term. This term has type $\forall P : \mathbb N \to Type, \forall z : P Z, \forall s : (\forall n : \mathbb N, P n \to P (S n)), \forall n, P (\pi_1 (t n))$ where $\pi_1$ is the first projection.
xavierm02
CC BY-SA 4.0
2018-08-09T17:24:26.900Z
(4) Prove (I don't remember how, there was probably some extra assumption involved) that $\pi_1 (t n) = n$, so that the term of step (3) is the induction principle.
xavierm02
CC BY-SA 4.0
2018-08-09T17:29:35.047Z
I think that this describes a way to achieve what you're trying to do: Impredicative Encodings of Inductive Types in HoTT.
xavierm02
CC BY-SA 4.0
2018-08-27T19:01:12.733Z
@xavierm02 I forgot commenting, but interesting idea/concept, thanks for the reference.
MaiaVictor
<type-theory><lambda-calculus><calculus-of-constructions>
Why isn't it "enough" to prove induction with one extra "INat" argument?
MaiaVictor
# Why isn't it "enough" to prove induction with one extra "INat" argument?

(Asked by: username_0 on 2018-08-09)

It is well known that it is impossible to prove the induction principle for Natural numbers on the Calculus of Constructions. That is,
Nat =
  ∀ P : *
  ∀ S : P -> P
  ∀ Z : P
  P

Zero =
  λ P : *
  λ S : P -> P
  λ Z : P
  Z

Succ =
  λ n : Nat
  λ P : *
  λ S : P -> P
  λ Z : P
  S (n P S Z)

NatInd :
  ∀ P : Nat -> *
  ∀ S : ∀ (n : Nat) -> P n -> P (Succ n)
  ∀ Z : P Zero
  ∀ n : Nat
  P n

There is no term of type NatInd on CoC, for either this or any other representation of Nat. But I've noticed that the following slightly different type can be constructed:
INat =
  λ n : Nat
  ∀ P : Nat -> *
  ∀ S : ∀ (n : Nat) -> P n -> P (S n)
  ∀ Z : P Zero
  P n

NatInd2 :
  ∀ P : Nat -> *
  ∀ S : ∀ (n : Nat) -> P n -> P (Succ n)
  ∀ Z : P Zero
  ∀ n : Nat
  ∀ i : INat n
  P n

Here, we first define a new type, INat : Nat -> *. That type is isomorphic to Nats and can be easily constructed for any natural number. Then, NatInd2 is a term that, given a proposition indexed on Nats, a base case Z, a step case S, for any nat n and its corresponding INat n, proves P(n) holds for every n. Or, in simpler words, NatInd2 is essentially induction, except that you must provide an additional argument i of type INat n, which you can always construct anyway. You could as well use dependent pairs to conveniently store Nat, INat pairs together.
It seems like this accomplishes the same one would expect from induction, i.e., you prove all cases from a base and a step case. Of course, there is an extra argument, but that argument is trivial to construct. For a "human reader", any proof using the method above would be equally convincing that some property holds for all n. So, my question is: is there any reason for the above method to be insufficient in general? Why is it so important to have the former unaltered definition of NatInd?

**Tags:** type-theory, lambda-calculus, calculus-of-constructions
> **Comments:**
> **username_1**: You have the type Nat which only has recursion, but not induction (i.e. the type of the result can't depend on the input). Then you build Nat2 (named INat) which allows you to have some kind of weak induction: if you give a Nat2 as input, then the type of the output can depend on a Nat.  
> **username_0**: @xavierm02 yes, I think that's more or less what I did. My question is pretty much "why that is not enough", perhaps in a philosophical sense? Because as I understand, an inductive proof using `NatInd2` would be equally "truthful" as an inductive proof using `NatInt`.  
> **username_1**: My intuition is that: (1) You will need to define Nat3, Nat4 etc. to do some things. (2) There may be (very weird convoluted?) things for which no Natn would work. (3) You may be interested in the trick to get induction from recursion plus induction for the equality type.  
> **username_1**: I'm not even convinced you can build an element of INat / Nat2.  
> **username_0**: @xavierm02 [here](https://gist.github.com/MaiaVictor/35b60441237510a0161450e278f952c8) is a construction of that INat. About (1), I think that is ok, can even be added automatically. About (2), maybe. About (3), do you have a name / reference for that trick?  
> **username_1**: The trick was something like this: (1) Change the domain to $\Sigma_{n:\mathbb N}P n$ to make it non-dependent. (2) Use the recursion principle to build a term $t$ of type $\forall P : \mathbb N \to Type, \forall z : P Z, \forall s : (\forall n : \mathbb N, P n \to P (S n)), \forall n, \Sigma_{n:\mathbb N}P n$ (3) Define the induction principle as the first projection of the previous term. This term has type $\forall P : \mathbb N \to Type, \forall z : P Z, \forall s : (\forall n : \mathbb N, P n \to P (S n)), \forall n, P (\pi_1 (t n))$ where $\pi_1$ is the first projection.  
> **username_1**: (4) Prove (I don't remember how, there was probably some extra assumption involved) that $\pi_1 (t n) = n$, so that the term of step (3) is the induction principle.  
> **username_1**: I think that this describes a way to achieve what you're trying to do: Impredicative Encodings of Inductive Types in HoTT.  
> **username_0**: @xavierm02 I forgot commenting, but interesting idea/concept, thanks for the reference.  

---

## 1 answers

### Answer by username_2 on 2018-08-14. Score: 6 | Accepted answer

Let us spell out the informal meaning of INat, IntNat and IndNat2. Suppose we have a predicate P on natural numbers. Say that P is inductive if we can inhabit P Zero and ∀ k . P k -> P (Succ k). Then we have:

NatInd P states "if P is inductive then, for all j : Nat, we have P j"
INat n P states "if P is inductive then P n"
NatInd2 P states: "if P is inductive and for every n we have an i which allows us to inhabit inductive predicates at n, then we can inhabit P n".

As you can see, NatInd2 just sweeps the problem under the rug, because it essentially asks that we give it a way of implementing induction. It is true that we can inhabit INat Zero, INat (Succ Zero), INat (Succ (Succ Zero)), ... but that does not imply that we can inhabit ∀ k . INat k! If you think otherwise, provide a term that does so.
In essence, you just hid the problem a little deeper by introducing a level of indirection. You could have already asked this: I can inhabit an infinite sequence of types NatInd P S Z Zero, NatInd P S Z (Succ Zero), NatInt P S Z (Succ (Succ Zero)), ... – why is this not sufficient to have induction? The answer: because you are suposed to inhabit ∀ n : Nat, NatInd P S Z n, which is not the same thing! The former is truth at the meta-level and the latter is an internal induction principle inside the calculus.
The question revolves around the difference between having an infinite sequence of terms inhabiting
t0 : Q 0
t1 : Q 1
t2 : Q 2
t3 : Q 3
...

versus having a single term
t : ∀ n : Nat, Q n

Given t, we can of course produce t0, t1, t2, etc. But there is generally no way to produce a t if we know that we have the infinite sequence of terms t0, t1, t2, ..., even in the case when there is an algorithm generating the sequence, for such an algorithm may not be expressible in the language (CiC in our case). Is that clear?
In fact, we can show that, given any (sufficiently expressive) strongly normalizing calculus (and a total language in general), there will be an instance of Q : Nat -> * such that we can inhabit each of Q 0, Q 1, Q 2, ... separately, but not ∀ n : Nat, Q n. This just says that no strongly normalizing calculus can express all total computable functions.
Supplemental: The OP is aksing why one needs, ought, or should internalize universal quantifiers. From a programmer's point of view the answer is simply that this is what is needed. Let us consider the practical difference between having an infinite sequence of terms
t0 : P 0
t1 : P 1
t2 : P 2
...

versus a single term
u : ∀ n : Nat, P n

Suppose you want to write a program which reads from the standard input a natural number k and outputs a witness of the statement P k. If we have u then we can do it easily (I am inventing syntax as I go here):
print "Please enter a natural number" ;
let k = input() in
print (u k)

How could we write such a program if instead of u we had a sequence of terms t0, t1, t2, as above? One could attempt something like
print "Please enter a natural number" ;
let k = input() in
if k = 0 then print t0
else if k = 1 then print t1
else if k = 2 then print t2
...

but this will not do because programs cannot be infinite. One could also try to do it as follows, assuming there is an algorithm A which produces the sequence t0, t1, t2 (but this algorithm is not expressible in our programming language):

The programmer asks the user to tell him a natural number.
The user provides a natural number k.
The programer runs A to get the expression tk of type P k.
The programer writes down the program print (u tk) and runs it.

We can see quite plainly that the programmer is now doing the job of the program, i.e., everything has moved to the meta-level, which is not what we want. We want the machines to do the job for us. You could also use a programming language which can express the algorithm A, but then you've switched to a different programming language and your algorithm A will correspond to the original program u.
The program u is needed because we must be able to compose and combine it with other pieces of code where it is not known in advance how u will be used.
We can also take the logical point of view. What is the difference between having at our disposal an infinite sequence of proofs
t0 : P 0
t1 : P 1
t2 : P 2
...

versus a single proof
u : ∀ n : Nat, P n

When we inspect u and verify that it is valid, we have provided evidence that P holds for all numbers. In contrast, the sequence of proofs t0, t1, t2, ... is not a finite amount of information, and so it cannot be verified and validated in finite time. Such infinite amount of information does not provide evidence that P holds for all numbers, at least not according to the standard that evidence in mathematics means proof. A proof by definition is finite and verifiable.
You may try to save the day by saying something like "but if we verify the algorithm that produces the sequence t0, t1, t2, ... then we will know that P holds for all n". This is true, but again, you're switching to the meta-level in which the verification that the algorithm works corresponds to having the proof u.

> **Comments:**
> **username_0**: I'm very sorry but I don't think that covers my doubt. I understand *"that does not imply that we can inhabit ∀ k . INat k"* but don't understand **why you should**, nor why *"you are suposed to inhabit ∀ n : Nat, NatInd P S Z n"*. I understand that there is not an algorithm on the language capable of producing `t0`, `t1`, `t2` given a `n : Nat`, but I don't understand **why, in practice, you need that**. What I see is that, anytime you'd use `NatInd`, you need a `n : Nat` to get a result. Anytime you'd use `NatInt2`, you need a `n : Nat` and `i : INat n`. So, what (...)  
> **username_0**: (...) I'm having trouble is figuring out "when", or "in what practical situation" `NatInt2` wouldn't be enough, because, in the context of "programming", anytime you can provide a `n` to `NatInt`, the programmer could just provide a pair `n, i` to `NatInt2` and get the same result. Similarly, if we take CoC as a formalization of mathematics, a proof of `∀ n : Nat . ∀ i : INat n . P n` would clearly imply that `P` truly holds for all `n` - which is what we want, right? So, in the context of proving mathematical theorems, I, too, I don't understand when `NatInt2` wouldn't suffice.  
> **username_0**: (I meant NatInd not NatInt. And sorry for making those additional comments, but I think I should be honest when I don't understand a point, despite being given a great explanation.)  
> **username_0**: Btw, `∀ n : Nat . ∀ i : INat n . P n` implies `∀ n : Nat . P n` because we can construct a `INat n` for all `n`, even though we can't do that inside the language (i.e., there is no proof of `∀ n : Nat -> INat n`). So, perhaps the issue is that it is somehow it is considered essential to have that last bit internalized, but what I don't get is, "why"? Again, for programming, the editor could just fill the `INat n`. For mathematics, anyone reading `∀ n : Nat . ∀ i : INat n . P n` would be equally convinced that `P n` holds for all `n`. Right?  
> **username_2**: It is false that `∀ n : Nat . ∀ i : INat n . P n` implies `∀ n : Nat . P n`. For that to be the case, you need to provide a term of type `(∀ n : Nat . ∀ i : INat n . P n) → ∀ n : Nat . P n`, which you cannot do. What you are observing is that *every instance* can be inahbited, which is useless from a programming point of view. I supplemented my answer with an explanation of why this is so.  
> **username_0**: The example made it obvious. Sorry for not getting it before.  

---

