Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ setprod u6 u6.
Claim L1: ap x0 0 ∈ u6
Apply ap0_Sigma with u6, λ x1 . u6, x0.
The subproof is completed by applying H0.
Claim L2: ap x0 u1 ∈ u6
Apply ap1_Sigma with u6, λ x1 . u6, x0.
The subproof is completed by applying H0.
Apply unknownprop_72649fc0d609625e17ac53e25cd57a51abe86f395cd11e949eac34127a9e2ea9 with ap x0 0, λ x1 x2 . lam 2 (λ x3 . If_i (x3 = 0) x2 (Church6_to_u6 (nth_6_tuple (ap x0 u1)))) = x0 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply unknownprop_72649fc0d609625e17ac53e25cd57a51abe86f395cd11e949eac34127a9e2ea9 with ap x0 u1, λ x1 x2 . lam 2 (λ x3 . If_i (x3 = 0) (ap x0 0) x2) = x0 leaving 2 subgoals.
The subproof is completed by applying L2.
Apply tuple_Sigma_eta with u6, λ x1 . u6, x0.
The subproof is completed by applying H0.
■