Let x0 of type ι → (ι → ι → ο) → (ι → ο) → ι → ι → ο be given.
Let x1 of type ι be given.
Let x2 of type ι → ι → ο be given.
Let x3 of type ι → ο be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Assume H0:
∀ x6 : ι → ι → ο . (∀ x7 . prim1 x7 x1 ⟶ ∀ x8 . prim1 x8 x1 ⟶ iff (x2 x7 x8) (x6 x7 x8)) ⟶ ∀ x7 : ι → ο . (∀ x8 . prim1 x8 x1 ⟶ iff (x3 x8) (x7 x8)) ⟶ x0 x1 x6 x7 x4 x5 = x0 x1 x2 x3 x4 x5.
Apply unknownprop_02f0cac4c02e49ce0f7220dcca6577c4622316d6aa3d6f676c744b755a99d67c with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x6 (2b2e3.. (f482f.. (363b9.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (363b9.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (363b9.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (363b9.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_97f1f10357220f1f8df31ca2897a79c3e582eb7b3b7efe8780fee275c21d2908 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (2b2e3.. (f482f.. (363b9.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (363b9.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (363b9.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) = x0 x1 x2 x3 x4 x5.
Apply unknownprop_686688eba3937d844c992740ce546d6832458df24b71cdd37efd735ee35fba33 with
x1,
x2,
x3,
x4,
x5,
λ x6 x7 . x0 x1 (2b2e3.. (f482f.. (363b9.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (decode_p (f482f.. (363b9.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6 = x0 x1 x2 x3 x4 x5.
Apply H0 with
2b2e3.. (f482f.. (363b9.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)),
decode_p (f482f.. (363b9.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))) leaving 2 subgoals.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply unknownprop_f9155e921425190d6d2642091acbb7921641a6733a0d0953d242b68d21270afb with
x1,
x2,
x3,
x4,
x5,
x6,
x7,
λ x8 x9 : ο . iff (x2 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying iff_refl with x2 x6 x7.
Let x6 of type ι be given.
Apply unknownprop_21b1a3136d7ac4765bfbef5c658131adbcc6bdea00fe52ebe3624f8fdbeaff24 with
x1,
x2,
x3,
x4,
x5,
x6,
λ x7 x8 : ο . iff (x3 x6) x7 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying iff_refl with x3 x6.