Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: int_lin_comb x0 x1 x2.

Let x3 of type ο be given.

Assume H1: ∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ add_SNo (mul_SNo x4 x0) (mul_SNo x5 x1) = x2 ⟶ x3.

Apply int_lin_comb_E with x0, x1, x2, x3 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H2: x0 ∈ int.

Assume H3: x1 ∈ int.

Assume H4: x2 ∈ int.

The subproof is completed by applying H1.

■

Proofgold Proof