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.
Assume H0: x2Pi x0 (λ x3 . x1 x3).
Apply SepE with prim4 (lam x0 (λ x3 . prim3 (x1 x3))), λ x3 . ∀ x4 . x4x0ap x3 x4x1 x4, x2, and (∀ x3 . x3x2and (pair_p x3) (ap x3 0x0)) (∀ x3 . x3x0ap x2 x3x1 x3) leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1: x2prim4 (lam x0 (λ x3 . prim3 (x1 x3))).
Assume H2: ∀ x3 . x3x0ap x2 x3x1 x3.
Apply andI with ∀ x3 . x3x2and (pair_p x3) (ap x3 0x0), ∀ x3 . x3x0ap x2 x3x1 x3 leaving 2 subgoals.
Let x3 of type ι be given.
Assume H3: x3x2.
Claim L4: x2lam x0 (λ x4 . prim3 (x1 x4))
Apply PowerE with lam x0 (λ x4 . prim3 (x1 x4)), x2.
The subproof is completed by applying H1.
Claim L5: x3lam x0 (λ x4 . prim3 (x1 x4))
Apply L4 with x3.
The subproof is completed by applying H3.
Apply andI with pair_p x3, ap x3 0x0 leaving 2 subgoals.
Claim L6: setsum (proj0 x3) (proj1 x3) = x3
Apply proj_Sigma_eta with x0, λ x4 . prim3 (x1 x4), x3.
The subproof is completed by applying L5.
Apply L6 with λ x4 x5 . pair_p x4.
The subproof is completed by applying pair_p_I with proj0 x3, proj1 x3.
Apply ap0_Sigma with x0, λ x4 . prim3 (x1 x4), x3.
The subproof is completed by applying L5.
The subproof is completed by applying H2.