Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
→
(
ι
→
ι
) →
ο
be given.
Assume H0:
∀ x1 .
∀ x2 :
ι → ι
.
(
∀ x3 .
x3
∈
x1
⟶
x2
x3
∈
x1
)
⟶
∀ x3 :
ι → ι
.
(
∀ x4 .
x4
∈
x1
⟶
x2
x4
=
x3
x4
)
⟶
x0
x1
x3
=
x0
x1
x2
.
Assume H1:
x0
1
(
λ x1 .
0
)
.
Assume H2:
x0
omega
(
λ x1 .
x1
)
.
Apply and5I with
MetaCat_terminal_p
(
λ x1 .
and
(
struct_u
x1
)
(
unpack_u_o
x1
x0
)
)
UnaryFuncHom
struct_id
struct_comp
(
pack_u
1
(
λ x1 .
0
)
)
(
λ x1 .
lam
(
ap
x1
0
)
(
λ x2 .
0
)
)
,
(
λ x1 .
and
(
struct_u
x1
)
(
unpack_u_o
x1
x0
)
)
(
pack_u
omega
(
λ x1 .
x1
)
)
,
UnaryFuncHom
(
pack_u
1
(
λ x1 .
0
)
)
(
pack_u
omega
(
λ x1 .
x1
)
)
(
lam
1
(
λ x1 .
0
)
)
,
UnaryFuncHom
(
pack_u
omega
(
λ x1 .
x1
)
)
(
pack_u
omega
(
λ x1 .
x1
)
)
(
lam
omega
(
λ x1 .
ordsucc
x1
)
)
,
∀ x1 x2 x3 .
...
⟶
...
⟶
...
⟶
and
(
and
(
and
(
UnaryFuncHom
(
pack_u
omega
(
λ x4 .
x4
)
)
x1
(
(
λ x4 x5 x6 .
lam
omega
(
λ x7 .
nat_primrec
(
ap
x5
0
)
(
λ x8 x9 .
ap
x6
x9
)
x7
)
)
x1
x2
x3
)
)
(
struct_comp
(
pack_u
1
(
λ x4 .
0
)
)
(
pack_u
omega
(
λ x4 .
x4
)
)
x1
(
(
λ x4 x5 x6 .
lam
omega
(
λ x7 .
nat_primrec
(
ap
x5
0
)
(
λ x8 x9 .
ap
x6
x9
)
x7
)
)
x1
x2
x3
)
(
lam
1
(
λ x4 .
0
)
)
=
x2
)
)
(
struct_comp
(
pack_u
omega
(
λ x4 .
x4
)
)
(
pack_u
omega
(
λ x4 .
x4
)
)
x1
(
(
λ x4 x5 x6 .
lam
omega
(
λ x7 .
nat_primrec
(
ap
x5
0
)
(
λ x8 x9 .
ap
x6
x9
)
x7
)
)
x1
x2
x3
)
(
lam
omega
(
λ x4 .
ordsucc
x4
)
)
=
struct_comp
(
pack_u
omega
(
λ x4 .
x4
)
)
x1
x1
x3
(
(
λ x4 x5 x6 .
lam
omega
(
λ x7 .
nat_primrec
(
ap
x5
0
)
(
λ x8 x9 .
ap
x6
x9
)
x7
)
)
x1
x2
x3
)
)
)
(
∀ x4 .
...
⟶
struct_comp
...
...
...
...
...
=
...
⟶
struct_comp
(
pack_u
omega
(
λ x5 .
x5
)
)
(
pack_u
omega
(
λ x5 .
x5
)
)
x1
x4
(
lam
omega
(
λ x5 .
ordsucc
x5
)
)
=
struct_comp
(
pack_u
omega
(
λ x5 .
x5
)
)
x1
x1
x3
x4
⟶
x4
=
(
λ x5 x6 x7 .
lam
omega
(
λ x8 .
nat_primrec
(
ap
x6
0
)
(
λ x9 x10 .
ap
x7
x10
)
x8
)
)
x1
x2
x3
)
leaving 5 subgoals.
...
...
...
...
...
■