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