Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_ca4ccf6887ff6dc7b05e5402a8b941f864c9703226396122edada9d3d18a208b with λ x0 x1 : ι → (ι → ο)(ι → ι) → ι . ∀ x2 . ∀ x3 : ι → ο . ∀ x4 : ι → ι . ∀ x5 . In x5 (x1 x2 (λ x6 . x3 x6) (λ x6 . x4 x6))∃ x6 . and (and (In x6 x2) (x3 x6)) (x5 = x4 x6).
Let x0 of type ι be given.
Let x1 of type ιο be given.
Let x2 of type ιι be given.
Let x3 of type ι be given.
Assume H0: In x3 (Repl (Sep x0 (λ x4 . x1 x4)) (λ x4 . x2 x4)).
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with Sep x0 (λ x4 . x1 x4), x2, x3, ∃ x4 . and (and (In x4 x0) (x1 x4)) (x3 = x2 x4) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x4 of type ι be given.
Assume H1: In x4 (Sep x0 (λ x5 . x1 x5)).
Assume H2: x3 = x2 x4.
Apply unknownprop_6a6b356f855b99f3fbff4effcb62e3ee6aa23839e10650eb28a503a368c2bb09 with x0, x1, x4, ∃ x5 . and (and (In x5 x0) (x1 x5)) (x3 = x2 x5) leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3: In x4 x0.
Assume H4: x1 x4.
Let x5 of type ο be given.
Assume H5: ∀ x6 . and (and (In x6 x0) (x1 x6)) (x3 = x2 x6)x5.
Apply H5 with x4.
Apply unknownprop_c7bf67064987d41cefc55afb6af6ecbbb6b830405f2005e0def6e504b3ca3bf3 with In x4 x0, x1 x4, x3 = x2 x4 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
The subproof is completed by applying H2.