Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Assume H0: prim1 x2 (3097a.. x0 (λ x3 . x1 x3)).

Let x3 of type ι be given.

Assume H1: prim1 x3 (3097a.. x0 (λ x4 . x1 x4)).

Assume H2: ∀ x4 . prim1 x4 x0 ⟶ f482f.. x2 x4 = f482f.. x3 x4.

Apply set_ext with x2, x3 leaving 2 subgoals.

Apply unknownprop_5e17df8b0eae318f4f7e08a9a5ed4289335a0d7cb9e03d231cf206660f20c5aa with x0, x1, x2, x3 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Let x4 of type ι be given.

Assume H3: prim1 x4 x0.

Apply H2 with x4, λ x5 x6 . Subq x6 (f482f.. x3 x4) leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying Subq_ref with f482f.. x3 x4.

Apply unknownprop_5e17df8b0eae318f4f7e08a9a5ed4289335a0d7cb9e03d231cf206660f20c5aa with x0, x1, x3, x2 leaving 3 subgoals.