Search for blocks/addresses/...

Proofgold Proof

pf
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.
Let x6 of type ιιι be given.
Let x7 of type ιιι be given.
Let x8 of type ιιο be given.
Assume H0: ∀ x9 . x9x0∀ x10 . x10x0x3 x9 x10 = x6 x9 x10.
Assume H1: ∀ x9 . x9x0∀ x10 . x10x0x4 x9 x10 = x7 x9 x10.
Assume H2: ∀ x9 . x9x0∀ x10 . x10x0iff (x5 x9 x10) (x8 x9 x10).
Apply iffI with explicit_Reals x0 x1 x2 x3 x4 x5, explicit_Reals x0 x1 x2 x6 x7 x8 leaving 2 subgoals.
Apply unknownprop_3b552f49d6c33f4d08ab7d5e3880cbc5e8e473340428bccc29909b64db43bcdc with x0, x1, x2, x3, x4, x5, x6, x7, x8 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_3b552f49d6c33f4d08ab7d5e3880cbc5e8e473340428bccc29909b64db43bcdc with x0, x1, x2, x6, x7, x8, x3, x4, x5 leaving 3 subgoals.
Let x9 of type ι be given.
Assume H3: x9x0.
Let x10 of type ι be given.
Assume H4: x10x0.
Let x11 of type ιιο be given.
Apply H0 with x9, x10, λ x12 x13 . x11 x13 x12 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Let x9 of type ι be given.
Assume H3: x9x0.
Let x10 of type ι be given.
Assume H4: x10x0.
Let x11 of type ιιο be given.
Apply H1 with x9, x10, λ x12 x13 . x11 x13 x12 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Let x9 of type ι be given.
Assume H3: x9x0.
Let x10 of type ι be given.
Assume H4: x10x0.
Apply iff_sym with x5 x9 x10, x8 x9 x10.
Apply H2 with x9, x10 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.