Claim L1:
(λ x0 . λ x1 : ι → ι . bij x0 x0 x1) 1 (λ x0 . 0)Apply bijI with
1,
1,
λ x0 . 0 leaving 3 subgoals.
Let x0 of type ι be given.
Assume H1: x0 ∈ 1.
The subproof is completed by applying In_0_1.
Let x0 of type ι be given.
Assume H1: x0 ∈ 1.
Let x1 of type ι be given.
Assume H2: x1 ∈ 1.
Assume H3: (λ x2 . 0) x0 = (λ x2 . 0) x1.
Apply cases_1 with
x0,
λ x2 . x2 = x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply cases_1 with
...,
... leaving 2 subgoals.
Claim L2:
(λ x0 . λ x1 : ι → ι . bij x0 x0 x1) omega (λ x0 . x0)The subproof is completed by applying bij_id with
omega.
Let x0 of type ο be given.
Apply H3 with
pack_u 1 (λ x1 . 0).
Let x1 of type ο be given.
Apply H4 with
λ x2 . lam (ap x2 0) (λ x3 . 0).
Let x2 of type ο be given.
Apply H5 with
pack_u omega (λ x3 . x3).
Let x3 of type ο be given.
Apply H6 with
lam 1 (λ x4 . 0).
Let x4 of type ο be given.
Apply H7 with
lam omega (λ x5 . ordsucc x5).
Let x5 of type ο be given.
Apply H8 with
λ x6 x7 x8 . lam omega (λ x9 . nat_primrec (ap x7 0) (λ x10 x11 . ap x8 x11) x9).
Apply unknownprop_1897dd9d62036e24b5a15a6305884877d2b2984b6fa2f5de30c61ce53aecce82 with
λ x6 . λ x7 : ι → ι . bij x6 x6 x7 leaving 3 subgoals.
The subproof is completed by applying L0.
The subproof is completed by applying L1.
The subproof is completed by applying L2.