Apply unknownprop_344c784b1c3b94c370e58970c6c07f9652a98f817bb26a71614a2661ed1216a6 with
λ x0 x1 . mul_nat 2 x0 = 32.
set y1 to be 32
Claim L0: ∀ x2 : ι → ο . x2 y1 ⟶ x2 y0
Let x2 of type ι → ο be given.
Assume H0: x2 32.
Apply mul_add_nat_distrL with
2,
8,
8,
λ x3 . x2 leaving 4 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_8.
The subproof is completed by applying nat_8.
Apply unknownprop_36374898b358f79d17b8b2339ff8c1fbf04a96c8611bd3a9eaa03c3fcb156f33 with
λ x3 x4 . add_nat x4 x4 = 32,
λ x3 . x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_de864b47665083064c24ffdfe59603868a4229c0f77319f6c6be7c92dbecbe0f.
The subproof is completed by applying H0.
Let x2 of type ι → ι → ο be given.
Apply L0 with
λ x3 . x2 x3 y1 ⟶ x2 y1 x3.
Assume H1: x2 y1 y1.
The subproof is completed by applying H1.