Apply unknownprop_32bc7778cd02b216f957f8c5e9693c4b58b7ca04a4ca47b5f3adb522add7dd35 with
5,
λ x0 . mul_nat (ap (lam 6 (λ x1 . If_i (x1 = 0) 1 (If_i (x1 = 1) 0 (If_i (x1 = 2) 0 (If_i (x1 = 3) 1 (If_i (x1 = 4) 0 1)))))) x0) (exp_nat 2 x0),
λ x0 x1 . x1 = 41 leaving 2 subgoals.
The subproof is completed by applying nat_5.
Apply tuple_6_5_eq with
1,
0,
0,
1,
0,
1,
λ x0 x1 . add_nat (Sigma_nat 5 (λ x2 . mul_nat ((λ x3 . ap (lam 6 (λ x4 . If_i (x4 = 0) 1 (If_i (x4 = 1) 0 (If_i (x4 = 2) 0 (If_i (x4 = 3) 1 (If_i (x4 = 4) 0 1)))))) x3) x2) (exp_nat 2 x2))) (mul_nat x1 (exp_nat 2 5)) = 41.
Apply unknownprop_6e31f7e63da1d74f4ea3ef967162bc5821029ffe1e451b13664a6e51a570dea7 with
exp_nat 2 5,
λ x0 x1 . add_nat (Sigma_nat 5 (λ x2 . mul_nat ((λ x3 . ap (lam 6 (λ x4 . If_i (x4 = 0) 1 (If_i (x4 = 1) 0 (If_i (x4 = 2) 0 (If_i (x4 = 3) 1 (If_i (x4 = 4) 0 1)))))) x3) x2) (exp_nat 2 x2))) x1 = 41 leaving 2 subgoals.
Apply unknownprop_1b73e01bc234ba0e318bc9baf16604d4f0fc12bea57885439d70438de4eb7174 with
2,
5 leaving 2 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_5.
Apply unknownprop_32bc7778cd02b216f957f8c5e9693c4b58b7ca04a4ca47b5f3adb522add7dd35 with
4,
λ x0 . mul_nat ((λ x1 . ap (lam 6 (λ x2 . If_i (x2 = 0) 1 (If_i (x2 = 1) 0 (If_i (x2 = 2) 0 (If_i (x2 = 3) 1 (If_i (x2 = 4) 0 1)))))) x1) x0) (exp_nat 2 x0),
λ x0 x1 . add_nat x1 (exp_nat 2 5) = 41 leaving 2 subgoals.
The subproof is completed by applying nat_4.