Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: In x2 (setexp x1 x0).

Let x3 of type ι be given.

Assume H1: In x3 x0.

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

Apply unknownprop_7e65b2cb934666fa04709e34a9ec7a8cd447de0a66d9962491fb608c410f4e23 with x0, x1, x2.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

■