Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H0: x0 = 0.
Apply andI with
struct_r (pack_r x0 x1),
unpack_r_o (pack_r x0 x1) (λ x2 . λ x3 : ι → ι → ο . and (and (and (∀ x4 . x4 ∈ x2 ⟶ not (x3 x4 x4)) (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ or (x3 x4 x5) (x3 x5 x4))) (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x6 ⟶ x3 x4 x6)) (∀ x4 : ι → ο . (∀ x5 . x5 ∈ x2 ⟶ (∀ x6 . x6 ∈ x2 ⟶ x3 x6 x5 ⟶ x4 x6) ⟶ x4 x5) ⟶ ∀ x5 . x5 ∈ x2 ⟶ x4 x5)) leaving 2 subgoals.
The subproof is completed by applying pack_struct_r_I with x0, x1.
Apply H0 with
λ x2 x3 . unpack_r_o (pack_r x3 x1) (λ x4 . λ x5 : ι → ι → ο . and (and (and (∀ x6 . x6 ∈ x4 ⟶ not (x5 x6 x6)) (∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ or (x5 x6 x7) (x5 x7 x6))) (∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ ∀ x8 . x8 ∈ x4 ⟶ x5 x6 x7 ⟶ x5 x7 x8 ⟶ x5 x6 x8)) (∀ x6 : ι → ο . (∀ x7 . x7 ∈ x4 ⟶ (∀ x8 . x8 ∈ x4 ⟶ x5 x8 x7 ⟶ x6 x8) ⟶ x6 x7) ⟶ ∀ x7 . x7 ∈ x4 ⟶ x6 x7)).
Apply unknownprop_34cda175c3cf01af70382673b777a4c5af85834006efe174637b2bbd21ba85af with
0,
x1,
λ x2 x3 : ο . x3.
Apply and4I with
∀ x2 . x2 ∈ 0 ⟶ not (x1 x2 x2),
∀ x2 . x2 ∈ 0 ⟶ ∀ x3 . x3 ∈ 0 ⟶ or (x1 x2 x3) (x1 x3 x2),
∀ x2 . x2 ∈ 0 ⟶ ∀ x3 . x3 ∈ 0 ⟶ ∀ x4 . x4 ∈ 0 ⟶ x1 x2 x3 ⟶ x1 x3 x4 ⟶ x1 x2 x4,
∀ x2 : ι → ο . (∀ x3 . x3 ∈ 0 ⟶ (∀ x4 . x4 ∈ 0 ⟶ x1 x4 x3 ⟶ x2 x4) ⟶ x2 x3) ⟶ ∀ x3 . x3 ∈ 0 ⟶ x2 x3 leaving 4 subgoals.
Let x2 of type ι be given.
Assume H1: x2 ∈ 0.
Apply FalseE with
not (x1 x2 x2).
Apply EmptyE with
x2.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H1: x2 ∈ 0.
Apply FalseE with
∀ x3 . x3 ∈ 0 ⟶ or (x1 x2 x3) (x1 x3 x2).
Apply EmptyE with
x2.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H1: x2 ∈ 0.
Apply FalseE with
∀ x3 . ... ⟶ ∀ x4 . ... ⟶ ... ⟶ x1 x3 ... ⟶ x1 x2 x4.