Proofgold Proof

pf

Claim L0: ∀ x0 . SelfInjection x0 ⟶ struct_u x0

Let x0 of type ι be given.

Assume H0: SelfInjection x0.

Apply H0 with struct_u x0.

Assume H1: struct_u x0.

Assume H2: unpack_u_o x0 (λ x1 . inj x1 x1).

The subproof is completed by applying H1.

Apply unknownprop_137f848bdb78f472068da9f3e5698255d8403888e1b30f209fd7da0af03ad2f1 with SelfInjection.

The subproof is completed by applying L0.

■