Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 02b90.. x0 x1.
Apply unknownprop_e277188ae242e07bd6727f267e38747aecd739d129890076e65b92339f7beb98 with x0, x1, ∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: and (and (and (80242.. (02a50.. x0 x1)) (prim1 (e4431.. (02a50.. x0 x1)) (4ae4a.. (0ac37.. (a842e.. x0 (λ x2 . 4ae4a.. (e4431.. x2))) (a842e.. x1 (λ x2 . 4ae4a.. (e4431.. x2))))))) (∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1))) (∀ x2 . prim1 x2 x1 ⟶ 099f3.. (02a50.. x0 x1) x2).
Assume H2: ∀ x2 . 80242.. x2 ⟶ (∀ x3 . prim1 x3 x0 ⟶ 099f3.. x3 x2) ⟶ (∀ x3 . prim1 x3 x1 ⟶ 099f3.. x2 x3) ⟶ and (Subq (e4431.. (02a50.. x0 x1)) (e4431.. x2)) (SNoEq_ (e4431.. (02a50.. x0 x1)) (02a50.. x0 x1) x2).
Apply H1 with ∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1).
Assume H3: and (and (80242.. (02a50.. x0 x1)) (prim1 (e4431.. (02a50.. x0 x1)) (4ae4a.. (0ac37.. (a842e.. x0 (λ x2 . 4ae4a.. (e4431.. x2))) (a842e.. x1 (λ x2 . 4ae4a.. (e4431.. x2))))))) (∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1)).
Assume H4: ∀ x2 . prim1 x2 x1 ⟶ 099f3.. (02a50.. x0 x1) x2.
Apply H3 with ∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1).
Assume H5: and (80242.. (02a50.. x0 x1)) (prim1 (e4431.. (02a50.. x0 x1)) (4ae4a.. (0ac37.. (a842e.. x0 (λ x2 . 4ae4a.. (e4431.. x2))) (a842e.. x1 (λ x2 . 4ae4a.. (e4431.. x2)))))).
Assume H6: ∀ x2 . prim1 x2 x0 ⟶ 099f3.. x2 (02a50.. x0 x1).
The subproof is completed by applying H6.
■