Apply unknownprop_f8cb4609f9c174a593de5a10197e2915f5c1a2d9f32ed8d30c3d30b788bb9e1e with λ x0 x1 : ι → ι → ι . ∀ x2 x3 . Subq x2 x3 ⟶ ∀ x4 x5 . Subq x4 x5 ⟶ Subq (x1 x2 x4) (x1 x3 x5).

Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: Subq x0 x1.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H1: Subq x2 x3.

Apply unknownprop_c64060985712f5c39c225eb3dab14c939b65a26a5915e1c104b0e622ec2f8a29 with x0, x1, λ x4 . x2, λ x4 . x3 leaving 2 subgoals.

The subproof is completed by applying H0.

Let x4 of type ι be given.

Assume H2: In x4 x0.

The subproof is completed by applying H1.

■

Proofgold Proof