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 : ι → ο . x1 x2 ⟶ x1 ((λ x3 : ι → ο . λ x4 . and (x3 x4) (x4 = prim0 (λ x5 . x3 x5) ⟶ ∀ x5 : ο . x5)) x2).
Assume H2:
∀ x2 : (ι → ο) → ο . (∀ x3 : ι → ο . x2 x3 ⟶ x1 x3) ⟶ x1 (Descr_Vo1 x2).
Apply H1 with
x0.
Apply H0 with
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.