Let x0 of type ι be given.
Let x1 of type (ι → ο) → ο be given.
Let x2 of type (ι → ο) → ο be given.
Assume H0:
∀ x3 : ι → ο . (∀ x4 . x3 x4 ⟶ prim1 x4 x0) ⟶ iff (x1 x3) (x2 x3).
Apply set_ext with
1216a.. (e5b72.. x0) (λ x3 . x1 (λ x4 . prim1 x4 x3)),
1216a.. (e5b72.. x0) (λ x3 . x2 (λ x4 . prim1 x4 x3)) leaving 2 subgoals.
Let x3 of type ι be given.
Apply unknownprop_e4362c04e65a765de9cf61045b78be0adc0f9e51a17754420e1088df0891ff67 with
e5b72.. x0,
λ x4 . x1 (λ x5 . prim1 x5 x4),
x3,
prim1 x3 (1216a.. (e5b72.. x0) (λ x4 . x2 (λ x5 . prim1 x5 x4))) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3:
x1 (λ x4 . prim1 x4 x3).
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with
e5b72.. x0,
λ x4 . x2 (λ x5 . prim1 x5 x4),
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply H0 with
λ x4 . prim1 x4 x3,
x2 (λ x4 . prim1 x4 x3) leaving 2 subgoals.
Apply unknownprop_4134b8a5d866cd7ad711ea569ada0ca0ba949f5cad571bf5782dc7c2d15cdb1c with
x0,
x3.
The subproof is completed by applying H2.
Assume H4:
x1 (λ x4 . prim1 x4 x3) ⟶ x2 (λ x4 . prim1 x4 x3).
Assume H5:
x2 (λ x4 . prim1 x4 x3) ⟶ x1 (λ x4 . prim1 x4 x3).
Apply H4.
The subproof is completed by applying H3.
Let x3 of type ι be given.
Apply unknownprop_e4362c04e65a765de9cf61045b78be0adc0f9e51a17754420e1088df0891ff67 with
e5b72.. x0,
λ x4 . x2 (λ x5 . prim1 x5 x4),
x3,
prim1 x3 (1216a.. (e5b72.. x0) (λ x4 . x1 (λ x5 . prim1 x5 x4))) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3:
x2 (λ x4 . prim1 x4 x3).
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with
e5b72.. x0,
λ x4 . x1 (λ x5 . prim1 x5 x4),
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply H0 with
λ x4 . prim1 x4 x3,
x1 (λ x4 . prim1 x4 x3) leaving 2 subgoals.
Apply unknownprop_4134b8a5d866cd7ad711ea569ada0ca0ba949f5cad571bf5782dc7c2d15cdb1c with
x0,
x3.
The subproof is completed by applying H2.
Assume H4:
x1 (λ x4 . prim1 x4 x3) ⟶ x2 (λ x4 . prim1 x4 x3).
Assume H5:
x2 (λ x4 . prim1 x4 x3) ⟶ x1 (λ x4 . prim1 x4 x3).
Apply H5.
The subproof is completed by applying H3.