Let x0 of type ι → ο be given.
Assume H0:
(λ x1 : ι → ο . ∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x2 ((λ x4 : ι → ο . λ x5 . and (x4 x5) (x5 = prim0 (λ x6 . x4 x6) ⟶ ∀ x6 : ο . x6)) x3)) ⟶ (∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x2 x4) ⟶ x2 (Descr_Vo1 x3)) ⟶ x2 x1) x0.
Let x1 of type ι → ο be given.
Assume H1:
(λ x2 : ι → ο . ∀ x3 : (ι → ο) → ο . (∀ x4 : ι → ο . x3 x4 ⟶ x3 ((λ x5 : ι → ο . λ x6 . and (x5 x6) (x6 = prim0 (λ x7 . x5 x7) ⟶ ∀ x7 : ο . x7)) x4)) ⟶ (∀ x4 : (ι → ο) → ο . (∀ x5 : ι → ο . x4 x5 ⟶ x3 x5) ⟶ x3 (Descr_Vo1 x4)) ⟶ x3 x2) x1.
Assume H2:
x1 (prim0 x0).
Apply unknownprop_55ac2036b2594a1420c3213980e6cc84263d48ba5c2b4b8c0dc5b53adbf2cdcc with
(λ x2 : ι → ο . λ x3 . and (x2 x3) (x3 = prim0 (λ x4 . x2 x4) ⟶ ∀ x4 : ο . x4)) x0,
x1,
∀ x2 . x0 x2 ⟶ x1 x2 leaving 4 subgoals.
Apply unknownprop_fc736d24ae94a3d5b74b9d45d9b476e94667edaaace7b4a17220d5e3dcc346ea with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H3:
∀ x2 . x1 x2 ⟶ (λ x3 : ι → ο . λ x4 . and (x3 x4) (x4 = prim0 (λ x5 . x3 x5) ⟶ ∀ x5 : ο . x5)) x0 x2.
Claim L4:
(λ x2 : ι → ο . λ x3 . and (x2 x3) (x3 = prim0 (λ x4 . x2 x4) ⟶ ∀ x4 : ο . x4)) x0 (prim0 x0)Apply H3 with
prim0 x0.
The subproof is completed by applying H2.
Apply andER with
x0 (prim0 x0),
prim0 x0 = prim0 x0 ⟶ ∀ x2 : ο . x2.
The subproof is completed by applying L4.
Apply L5 with
∀ x2 . x0 x2 ⟶ x1 x2.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H6.
Assume H3:
∀ x2 . (λ x3 : ι → ο . λ x4 . and (x3 x4) (x4 = prim0 (λ x5 . x3 x5) ⟶ ∀ x5 : ο . x5)) x0 x2 ⟶ x1 x2.
Let x2 of type ι be given.
Assume H4: x0 x2.
Apply xm with
x2 = prim0 x0,
x1 x2 leaving 2 subgoals.
Assume H5:
x2 = prim0 x0.
Apply H5 with
λ x3 x4 . x1 x4.
The subproof is completed by applying H2.
Assume H5:
x2 = prim0 x0 ⟶ ∀ x3 : ο . x3.
Apply H3 with
x2.
Apply andI with
x0 x2,
x2 = prim0 x0 ⟶ ∀ x3 : ο . x3 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.