Potential unsoundness in `fun::fnat::para_pre_zero` (`(n : nat) ⋀ (0 == n + 1) => false`)

[bvssvni]

The theorem is not incorrect, but I am concerned that the proof is not sound:

/// `(n : nat) ⋀ (0 == n + 1)  =>  false`.
pub fn para_pre_zero<N: Prop>((ty_n, x): And<Ty<N, Nat>, Eq<Zero, Inc<N>>>) -> False {
    match nat_def::<N, N>(ty_n.clone()) {
        Left(eq_n_zero) => para_eq_zero_one(eq::transitivity(x, app_eq(eq_n_zero))),
        Right(t) => para_eq_inc((ty_n.clone(), lam_app_nop(ty_n).0(t.1))),
    }
}

If one takes a look at nat_def:

/// `(x : nat)  =>  (x == 0) ⋁ (y : nat, (\(y : nat) = x == (y + 1))(y))`.
pub fn nat_def<X: Prop, Y: Prop>(
    _x_ty: Ty<X, Nat>
) -> Either<Eq<X, Zero>, DepTupTy<Y, Nat, Lam<Ty<Y, Nat>, Eq<X, Inc<Y>>>>> {unimplemented!()}

I make Y = X = N and this is what I find non-intuitive, that I can "force" Y to equal something and use it as a contradiction.

*Edit: The solution was to add prev(x).

[bvssvni]

One idea is to require theory(x == y) in nat_def.

[bvssvni]

There is another reason this is unsound: It accesses the second tuple component t.1:

error[E0616]: field `1` of struct `tup::Tup` is private
  --> src/fun/fnat.rs:53:70
   |
53 |         Right(t) => para_eq_inc((ty_n.clone(), lam_app_nop(ty_n).0(t.1))),
   |                                                                      ^ private field

This was found by moving Tup to its own module.

[bvssvni]

One idea is to use ~!x instead of y.

[bvssvni]

A better idea might be to use prev(x) instead of y. This has a unique meaning avoids complex collisions.