Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Let x3 of type ι be given.
Let x4 of type ι → ι → ι be given.
Apply explicit_Nats_E with
x0,
x1,
x2,
∀ x5 . a813b.. x0 x1 x2 x3 x4 x1 x5 ⟶ x5 = x3.
Assume H3:
∀ x5 . prim1 x5 x0 ⟶ x2 x5 = x1 ⟶ ∀ x6 : ο . x6.
Assume H4:
∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x5 = x2 x6 ⟶ x5 = x6.
Assume H5:
∀ x5 : ι → ο . x5 x1 ⟶ (∀ x6 . x5 x6 ⟶ x5 (x2 x6)) ⟶ ∀ x6 . prim1 x6 x0 ⟶ x5 x6.
Claim L6: (λ x5 x6 . x5 = x1 ⟶ x6 = x3) x1 x3
Assume H6: x1 = x1.
Let x5 of type ι → ι → ο be given.
Assume H7: x5 x3 x3.
The subproof is completed by applying H7.
Claim L7:
∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . (λ x7 x8 . x7 = x1 ⟶ x8 = x3) x5 x6 ⟶ (λ x7 x8 . x7 = x1 ⟶ x8 = x3) (x2 x5) (x4 x5 x6)Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H8: (λ x7 x8 . x7 = x1 ⟶ x8 = x3) x5 x6.
Assume H9: x2 x5 = x1.
Apply FalseE with
x4 x5 x6 = x3.
Apply H3 with
x5 leaving 2 subgoals.
The subproof is completed by applying H7.
The subproof is completed by applying H9.
Let x5 of type ι be given.
Assume H8:
a813b.. x0 x1 x2 x3 x4 x1 x5.
Apply H8 with
λ x6 x7 . x6 = x1 ⟶ x7 = x3 leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
Let x6 of type ι → ι → ο be given.
Assume H9: x6 x1 x1.
The subproof is completed by applying H9.