Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: equip x0 x1.
Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with x0, x1, equip (setprod x0 1) x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ιι be given.
Assume H1: bij x0 x1 x2.
Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with x0, x1, x2, equip (setprod x0 1) x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H2: inj x0 x1 x2.
Assume H3: ∀ x3 . In x3 x1∃ x4 . and (In x4 x0) (x2 x4 = x3).
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with x0, x1, x2, equip (setprod x0 1) x1 leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H4: ∀ x3 . In x3 x0In (x2 x3) x1.
Assume H5: ∀ x3 . In x3 x0∀ x4 . In x4 x0x2 x3 = x2 x4x3 = x4.
Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with setprod x0 1, x1, λ x3 . x2 (proj0 x3).
Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with setprod x0 1, x1, λ x3 . x2 (proj0 x3) leaving 2 subgoals.
Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with setprod x0 1, x1, λ x3 . x2 (proj0 x3) leaving 2 subgoals.
Let x3 of type ι be given.
Assume H6: In x3 (setprod x0 1).
Apply H4 with proj0 x3.
Apply unknownprop_7f5f9419800f93e9599d730a17dd65429a394b027111e15ab002441897ba80db with x0, 1, x3.
The subproof is completed by applying H6.
Let x3 of type ι be given.
Assume H6: In x3 (setprod x0 1).
Let x4 of type ι be given.
Assume H7: In x4 (setprod x0 1).
Assume H8: x2 (proj0 x3) = x2 (proj0 x4).
Apply unknownprop_25d0316470b9bdc33df1b5827718337aefe32f6ee5207178fa8d15f5c0f986af with x0, 1, x3, λ x5 x6 . x5 = x4 leaving 2 subgoals.
The subproof is completed by applying H6.
Apply unknownprop_25d0316470b9bdc33df1b5827718337aefe32f6ee5207178fa8d15f5c0f986af with x0, 1, x4, λ x5 x6 . lam 2 (λ x7 . If_i (x7 = 0) (ap x3 0) (ap x3 1)) = x5 leaving 2 subgoals.
The subproof is completed by applying H7.
Apply unknownprop_3189570886a432a72e87efcbd0ea995fafcd88c6ec3c7fdffceb2e344a826cdc with x3, λ x5 x6 . x5 = ap x4 0, λ x5 x6 . lam 2 (λ x7 . If_i (x7 = 0) x6 (ap x3 1)) = lam 2 (λ x7 . If_i (x7 = 0) (ap x4 0) (ap x4 1)) leaving 2 subgoals.
Apply unknownprop_3189570886a432a72e87efcbd0ea995fafcd88c6ec3c7fdffceb2e344a826cdc with x4, λ x5 x6 . proj0 x3 = x5.
Apply H5 with proj0 x3, proj0 x4 leaving 3 subgoals.
Apply unknownprop_7f5f9419800f93e9599d730a17dd65429a394b027111e15ab002441897ba80db with x0, 1, x3.
The subproof is completed by applying H6.
Apply unknownprop_7f5f9419800f93e9599d730a17dd65429a394b027111e15ab002441897ba80db with x0, 1, x4.
The subproof is completed by applying H7.
The subproof is completed by applying H8.
set y5 to be ...
Claim L9: ...
...
set y6 to be λ x6 x7 . lam 2 (λ x8 . If_i (x8 = 0) (ap y5 0) x7) = lam 2 (λ x8 . If_i (x8 = 0) (ap y5 0) ...)
Apply L9 with λ x7 . y6 x7 y5y6 y5 x7 leaving 2 subgoals.
Assume H10: y6 y5 y5.
The subproof is completed by applying H10.
Let x7 of type ιιο be given.
Assume H10: x7 (lam 2 (λ x8 . If_i (x8 = 0) (ap y6 0) (ap y6 1))) (lam 2 (λ x8 . If_i (x8 = 0) (ap y6 0) (ap y6 1))).
The subproof is completed by applying H10.
...