Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 74b16.. x0.
Apply H0 with λ x1 . x1 = 8e582.. (f482f.. x1 4a7ef..) (e3162.. (f482f.. x1 (4ae4a.. 4a7ef..))) (e3162.. (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. x1 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Assume H1: ∀ x3 . prim1 x3 x1 ⟶ ∀ x4 . prim1 x4 x1 ⟶ prim1 (x2 x3 x4) x1.
Let x3 of type ι → ι → ι be given.
Assume H2: ∀ x4 . prim1 x4 x1 ⟶ ∀ x5 . prim1 x5 x1 ⟶ prim1 (x3 x4 x5) x1.
Let x4 of type ι → ι → ο be given.
Let x5 of type ι → ι → ο be given.
Apply unknownprop_96e325f5225007f883608ced691e198c9132e00df04ef6b043937abf9b283533 with x1, x2, x3, x4, x5, λ x6 x7 . 8e582.. x1 x2 x3 x4 x5 = 8e582.. x6 (e3162.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (2b2e3.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (2b2e3.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).
Apply unknownprop_984bfacc3ef53e27098bfec28645a049a46d0b0ec9ea58f69ed9acc3b2c7db29 with x1, x2, e3162.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, 2b2e3.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, 2b2e3.. (f482f.. (8e582.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.
The subproof is completed by applying unknownprop_e5de091bc243fc8af09a52f41bd7457d930b22a1ee185a483ac9d233b589104d with x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_64e46c7a48eac1f7008652d9ab91808a3afbbfe70ec8208c5ad3733a08258cf5 with x1, x2, x3, x4, x5.
Let x6 of type ι be given.
Assume H3: prim1 x6 x1.
Let x7 of type ι be given.
Assume H4: prim1 x7 x1.
Apply unknownprop_41bee463d2b841a1f67904f27e4108ff00fd68bb9c970dddc779208040bf4303 with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x4 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying iff_refl with x4 x6 x7.
Let x6 of type ι be given.
Assume H3: prim1 x6 x1.
Let x7 of type ι be given.
Assume H4: prim1 x7 x1.
Apply unknownprop_2ef8d35badf747d6423713318afe09404bd82f4166069eb04b62dba2a480a3f4 with x1, x2, x3, x4, x5, x6, x7, λ x8 x9 : ο . iff (x5 x6 x7) x8 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying iff_refl with x5 x6 x7.
■