Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Assume H0: nat_p x2.

Apply nat_ind with λ x3 . and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 1) leaving 2 subgoals.

Apply add_nat_0R with x2, λ x3 x4 . and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 x4) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 x4) 1).

Apply andI with ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 x2) 0, ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 x2) 1 leaving 2 subgoals.

The subproof is completed by applying Subq_ref with ap (SNo_sqrtaux x0 x1 x2) 0.

The subproof is completed by applying Subq_ref with ap (SNo_sqrtaux x0 x1 x2) 1.

Let x3 of type ι be given.

Assume H1: nat_p x3.

Assume H2: and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 1).

Apply H2 with and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 (ordsucc x3))) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 (ordsucc x3))) 1).

Assume H3: ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 0.

Assume H4: ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 (add_nat x2 x3)) 1.

Apply add_nat_SR with x2, x3, λ x4 x5 . and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap (SNo_sqrtaux x0 x1 x5) 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap (SNo_sqrtaux x0 x1 x5) 1) leaving 2 subgoals.

The subproof is completed by applying H1.

Apply SNo_sqrtaux_S with x0, x1, add_nat x2 x3, λ x4 x5 . and (ap (SNo_sqrtaux x0 x1 x2) 0 ⊆ ap x5 0) (ap (SNo_sqrtaux x0 x1 x2) 1 ⊆ ap x5 1) leaving 2 subgoals.

Apply add_nat_p with x2, x3 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

...

■

Proofgold Proof