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