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: x0x2.
Assume H1: x1x2.
Apply tuple_2_eta with x0, x1, λ x3 x4 . x3setexp x2 2.
Apply lam_Pi with 2, λ x3 . x2, λ x3 . ap (lam 2 (λ x4 . If_i (x4 = 0) x0 x1)) x3.
Let x3 of type ι be given.
Assume H2: x32.
Apply cases_2 with x3, λ x4 . ap (lam 2 (λ x5 . If_i (x5 = 0) x0 x1)) x4x2 leaving 3 subgoals.
The subproof is completed by applying H2.
Apply tuple_2_0_eq with x0, x1, λ x4 x5 . x5x2.
The subproof is completed by applying H0.
Apply tuple_2_1_eq with x0, x1, λ x4 x5 . x5x2.
The subproof is completed by applying H1.