Claim L0: ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3) ⟶ 0ac37.. (91630.. 4a7ef..) (94f9e.. x0 (λ x3 . x1 x3)) = 0ac37.. (91630.. 4a7ef..) (94f9e.. x0 (λ x3 . x2 x3))

Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι → ι be given.

Assume H0: ∀ x3 . prim1 x3 x0 ⟶ x1 x3 = x2 x3.

Claim L1: 94f9e.. x0 (λ x3 . x1 x3) = 94f9e.. x0 (λ x3 . x2 x3)

Apply unknownprop_59be5eee144fb0f12156456c7f9888c3f0525fea126d0d8cdf71e5c53005d86a with x0, x1, x2.

The subproof is completed by applying H0.

Apply L1 with λ x3 x4 . 0ac37.. (91630.. 4a7ef..) x4 = 0ac37.. (91630.. 4a7ef..) (94f9e.. x0 (λ x5 . x2 x5)).

Let x3 of type ι → ι → ο be given.

Assume H2: x3 (0ac37.. (91630.. 4a7ef..) (94f9e.. x0 (λ x4 . x2 x4))) (0ac37.. (91630.. 4a7ef..) (94f9e.. x0 (λ x4 . x2 x4))).

The subproof is completed by applying H2.

Apply In_rec_i_eq with λ x0 . λ x1 : ι → ι . 0ac37.. (91630.. 4a7ef..) (94f9e.. x0 (λ x2 . x1 x2)).

The subproof is completed by applying L0.

■

Proofgold Proof