Let x and y be given.

Assume Hx Hy.

Let u be given.

Assume Hu.

Let p be given.

Assume Hp1 Hp2.

Apply mul_SNo_SNoL_interpolate x y Hx Hy u Hu to the current goal.

Assume H1.

Apply H1 to the current goal.

Let v be given.

Assume H1.

Apply H1 to the current goal.

Assume Hv.

Assume H1.

Apply H1 to the current goal.

Let w be given.

Assume H1.

Apply H1 to the current goal.

Assume Hw Hvw.

An exact proof term for the current goal is Hp1 v Hv w Hw Hvw.

Assume H1.

Apply H1 to the current goal.

Let v be given.

Assume H1.

Apply H1 to the current goal.

Assume Hv.

Assume H1.

Apply H1 to the current goal.

Let w be given.

Assume H1.

Apply H1 to the current goal.

Assume Hw Hvw.

An exact proof term for the current goal is Hp2 v Hv w Hw Hvw.

∎