Let x0 of type ι be given.
Let x1 of type (ι → ο) → ο be given.
Let x2 of type ι → ο be given.
Assume H0:
∀ x3 . x2 x3 ⟶ prim1 x3 x0.
Apply prop_ext_2 with
decode_c (e0e40.. x0 x1) x2,
x1 x2 leaving 2 subgoals.
Apply H1 with
x1 x2.
Let x3 of type ι be given.
Apply H2 with
x1 x2.
Assume H3:
∀ x4 . iff (x2 x4) (prim1 x4 x3).
Claim L5:
x1 (λ x4 . prim1 x4 x3)Apply unknownprop_e75b5686f39ea4dca8e72e616b0514162494e9e895f52dbe14fa1984a713fe57 with
e5b72.. x0,
λ x4 . x1 (λ x5 . prim1 x5 x4),
x3.
The subproof is completed by applying H4.
Claim L6:
(λ x4 . prim1 x4 x3) = x2Apply pred_ext_2 with
λ x4 . prim1 x4 x3,
x2 leaving 2 subgoals.
Let x4 of type ι be given.
Apply H3 with
x4,
(λ x5 . prim1 x5 x3) x4 ⟶ x2 x4.
Assume H6:
x2 x4 ⟶ prim1 x4 x3.
Assume H7:
prim1 x4 x3 ⟶ x2 x4.
The subproof is completed by applying H7.
Let x4 of type ι be given.
Apply H3 with
x4,
x2 x4 ⟶ (λ x5 . prim1 x5 x3) x4.
Assume H6:
x2 x4 ⟶ prim1 x4 x3.
Assume H7:
prim1 x4 x3 ⟶ x2 x4.
The subproof is completed by applying H6.
Apply L6 with
λ x4 x5 : ι → ο . x1 x4.
The subproof is completed by applying L5.
Assume H1: x1 x2.
Let x3 of type ο be given.
Apply H2 with
1216a.. x0 x2.
Apply andI with
∀ x4 . iff (x2 x4) (prim1 x4 (1216a.. x0 x2)),
prim1 (1216a.. x0 x2) (e0e40.. x0 x1) leaving 2 subgoals.
Let x4 of type ι be given.
Apply iffI with
x2 x4,
prim1 x4 (1216a.. x0 x2) leaving 2 subgoals.
Assume H3: x2 x4.
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with
x0,
x2,
x4 leaving 2 subgoals.
Apply H0 with
x4.
The subproof is completed by applying H3.
The subproof is completed by applying H3.
Apply unknownprop_e75b5686f39ea4dca8e72e616b0514162494e9e895f52dbe14fa1984a713fe57 with
x0,
x2,
x4.
The subproof is completed by applying H3.
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with
e5b72.. x0,
λ x4 . x1 (λ x5 . prim1 x5 x4),
1216a.. x0 x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_04c97c2c2d1a8e1962ff0429ce82d65b677812398d5dd7ead59c810d35c83fce with x0, x2.
Apply pred_ext_2 with
x2,
λ x4 . prim1 x4 (1216a.. x0 x2) leaving 2 subgoals.
Let x4 of type ι be given.
Assume H3: x2 x4.
Apply unknownprop_1dada0fb38ff7f9b45b564ad11d6295d93250427446875218f17ee62431454a6 with
x0,
x2,
x4 leaving 2 subgoals.
Apply H0 with
x4.
The subproof is completed by applying H3.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Apply unknownprop_e75b5686f39ea4dca8e72e616b0514162494e9e895f52dbe14fa1984a713fe57 with
x0,
x2,
x4.
The subproof is completed by applying H3.
Apply L3 with
λ x4 x5 : ι → ο . x1 x4.
The subproof is completed by applying H1.