Let x0 of type ι → ο be given.
Apply unknownprop_493b888cf0a805cead4e0248c971e6024ce25a1b7b03912f4ef24a0673efc991 with
λ x1 : ι → ο . and ((λ 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) (∀ x2 . x0 x2 ⟶ x1 x2).
Let x1 of type ι → ο be given.
Assume H0:
and ((λ 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) (∀ x2 . x0 x2 ⟶ x1 x2).
Apply andEL with
(λ 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,
∀ x2 . x0 x2 ⟶ x1 x2.
The subproof is completed by applying H0.