Apply unknownprop_58ff2b27b026e86dd7175f8c18dac8fe76e7f12b4c3407557df1571fd66d2cbc with
λ x0 x1 . mul_nat 2 x0 = 16.
set y1 to be 16
Claim L0: ∀ x2 : ι → ο . x2 y1 ⟶ x2 y0
Let x2 of type ι → ο be given.
Assume H0: x2 16.
Apply mul_add_nat_distrL with
2,
4,
4,
λ x3 . x2 leaving 4 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_4.
The subproof is completed by applying nat_4.
Apply unknownprop_82b4ca10eb7ca03c2ab8db9622e8ff501b1df3632d9b511d2313d8304ef45b38 with
λ x3 x4 . add_nat x4 x4 = 16,
λ x3 . x2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_344c784b1c3b94c370e58970c6c07f9652a98f817bb26a71614a2661ed1216a6.
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.