Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι → ο be given.
Assume H0: x0 4a7ef...
Assume H1: ∀ x1 . ba9d8.. x1 ⟶ x0 x1 ⟶ x0 (4ae4a.. x1).
Claim L2: and (ba9d8.. 4a7ef..) (x0 4a7ef..)
Apply andI with ba9d8.. 4a7ef.., x0 4a7ef.. leaving 2 subgoals.
The subproof is completed by applying unknownprop_e5c1596f5fd6bc2d713145a4e9d44688423a48751f219f9d9d142effb814941e.
The subproof is completed by applying H0.
Claim L3: ∀ x1 . and (ba9d8.. x1) (x0 x1) ⟶ and (ba9d8.. (4ae4a.. x1)) (x0 (4ae4a.. x1))
Let x1 of type ι be given.
Assume H3: and (ba9d8.. x1) (x0 x1).
Apply H3 with and (ba9d8.. (4ae4a.. x1)) (x0 (4ae4a.. x1)).
Assume H4: ba9d8.. x1.
Assume H5: x0 x1.
Apply andI with ba9d8.. (4ae4a.. x1), x0 (4ae4a.. x1) leaving 2 subgoals.
Apply unknownprop_11171438c9340577bc5ca6838eccea0ebdb4279227053bf618ee42741f7851b4 with x1.
The subproof is completed by applying H4.
Apply H1 with x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Assume H4: ba9d8.. x1.
Claim L5: and (ba9d8.. x1) (x0 x1)
Apply H4 with λ x2 . and (ba9d8.. x2) (x0 x2) leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
Apply andER with ba9d8.. x1, x0 x1.
The subproof is completed by applying L5.
■