Let x0 of type ι → ο be given.
Apply andI with
x0 (pack_r 1 (λ x1 x2 . True)),
∀ x1 . x0 x1 ⟶ and (BinRelnHom x1 (pack_r 1 (λ x2 x3 . True)) (lam (ap x1 0) (λ x2 . 0))) (∀ x2 . BinRelnHom x1 (pack_r 1 (λ x3 x4 . True)) x2 ⟶ x2 = (λ x3 . lam (ap x3 0) (λ x4 . 0)) x1) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Assume H2: x0 x1.
Apply H0 with
x1,
λ x2 . and (BinRelnHom x2 (pack_r 1 (λ x3 x4 . True)) (lam (ap x2 0) (λ x3 . 0))) (∀ x3 . BinRelnHom x2 (pack_r 1 (λ x4 x5 . True)) x3 ⟶ x3 = (λ x4 . lam (ap x4 0) (λ x5 . 0)) x2) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Let x3 of type ι → ι → ο be given.
Apply andI with
BinRelnHom (pack_r x2 x3) (pack_r 1 (λ x4 x5 . True)) (lam (ap (pack_r x2 x3) 0) (λ x4 . 0)),
∀ x4 . BinRelnHom (pack_r x2 x3) (pack_r 1 (λ x5 x6 . True)) x4 ⟶ x4 = (λ x5 . lam (ap x5 0) (λ x6 . 0)) (pack_r x2 x3) leaving 2 subgoals.
Apply pack_r_0_eq2 with
x2,
x3,
λ x4 x5 . BinRelnHom (pack_r x2 x3) (pack_r 1 (λ x6 x7 . True)) (lam x4 (λ x6 . 0)).
Apply unknownprop_4e486761c3790f4990f398ce8c16ea7ac5915924a294f8e5b06e45030e68e983 with
x2,
1,
x3,
λ x4 x5 . True,
lam x2 (λ x4 . 0),
λ x4 x5 : ο . x5.
Apply andI with
lam x2 (λ x4 . 0) ∈ setexp 1 x2,
∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ⟶ (λ x6 x7 . True) (ap (lam x2 (λ x6 . 0)) x4) (ap (lam x2 (λ x6 . 0)) x5) leaving 2 subgoals.
Apply lam_Pi with
x2,
λ x4 . 1,
λ x4 . 0.
Let x4 of type ι be given.
Assume H3: x4 ∈ x2.
The subproof is completed by applying In_0_1.
Let x4 of type ι be given.
Assume H3: x4 ∈ x2.
Let x5 of type ι be given.
Assume H4: x5 ∈ x2.
Assume H5: x3 x4 x5.
The subproof is completed by applying TrueI.
Let x4 of type ι be given.
Apply unknownprop_4e486761c3790f4990f398ce8c16ea7ac5915924a294f8e5b06e45030e68e983 with
x2,
1,
x3,
λ x5 x6 . True,
x4,
λ x5 x6 : ο . x6 ⟶ x4 = (λ x7 . lam (ap x7 0) (λ x8 . 0)) (pack_r x2 x3).
Assume H3:
and (x4 ∈ setexp 1 x2) (∀ x5 . x5 ∈ x2 ⟶ ∀ x6 . x6 ∈ x2 ⟶ x3 x5 x6 ⟶ True).
Apply H3 with
x4 = (λ x5 . lam (ap x5 0) (λ x6 . 0)) (pack_r x2 x3).
Assume H4:
x4 ∈ Pi x2 (λ x5 . 1).