Let x0 of type ι → ο be given.
Assume H1:
x0 (pack_b 0 (λ x1 x2 . x1)).
Apply andI with
x0 (pack_b 0 (λ x1 x2 . x1)),
∀ x1 . x0 x1 ⟶ and (MagmaHom (pack_b 0 (λ x2 x3 . x2)) x1 ((λ x2 . lam 0 (λ x3 . x3)) x1)) (∀ x2 . MagmaHom (pack_b 0 (λ x3 x4 . x3)) x1 x2 ⟶ x2 = (λ x3 . lam 0 (λ x4 . x4)) 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 (MagmaHom (pack_b 0 (λ x3 x4 . x3)) x2 ((λ x3 . lam 0 (λ x4 . x4)) x2)) (∀ x3 . MagmaHom (pack_b 0 (λ x4 x5 . x4)) x2 x3 ⟶ x3 = (λ x4 . lam 0 (λ x5 . x5)) x2) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Let x3 of type ι → ι → ι be given.
Assume H3: ∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ∈ x2.
Apply andI with
MagmaHom (pack_b 0 (λ x4 x5 . x4)) (pack_b x2 x3) ((λ x4 . lam 0 (λ x5 . x5)) (pack_b x2 x3)),
∀ x4 . MagmaHom (pack_b 0 (λ x5 x6 . x5)) (pack_b x2 x3) x4 ⟶ x4 = (λ x5 . lam 0 (λ x6 . x6)) (pack_b x2 x3) leaving 2 subgoals.
Apply unknownprop_7ee20a9b005b9d1cb4acab7f037a1615344131a99780aaa35f8fa78a1fc7660f with
0,
x2,
λ x4 x5 . x4,
x3,
lam 0 (λ x4 . x4),
λ x4 x5 : ο . x5.
Apply andI with
lam 0 (λ x4 . x4) ∈ setexp x2 0,
∀ x4 . x4 ∈ 0 ⟶ ∀ x5 . x5 ∈ 0 ⟶ ap (lam 0 (λ x6 . x6)) ((λ x6 x7 . x6) x4 x5) = x3 (ap (lam 0 (λ x6 . x6)) x4) (ap (lam 0 (λ x6 . x6)) x5) leaving 2 subgoals.
Apply lam_Pi with
0,
λ x4 . x2,
λ x4 . x4.
Let x4 of type ι be given.
Assume H4: x4 ∈ 0.
Apply FalseE with
(λ x5 . x5) x4 ∈ (λ x5 . x2) x4.
Apply EmptyE with
x4.
The subproof is completed by applying H4.
Let x4 of type ι be given.
Assume H4: x4 ∈ 0.
Apply FalseE with
∀ x5 . x5 ∈ 0 ⟶ ap (lam 0 (λ x6 . x6)) ((λ x6 x7 . x6) x4 x5) = x3 (ap (lam 0 (λ x6 . x6)) x4) (ap (lam 0 (λ x6 . x6)) x5).
Apply EmptyE with
x4.
The subproof is completed by applying H4.
Let x4 of type ι be given.
Apply unknownprop_7ee20a9b005b9d1cb4acab7f037a1615344131a99780aaa35f8fa78a1fc7660f with
0,
x2,
λ x5 x6 . x5,
x3,
x4,
λ x5 x6 : ο . x6 ⟶ x4 = (λ x7 . lam 0 (λ x8 . x8)) (pack_b x2 x3).
Assume H4:
and (x4 ∈ setexp x2 0) (∀ x5 . ... ⟶ ∀ x6 . ... ⟶ ap x4 ((λ x7 x8 . x7) ... ...) = ...).