Proofgold Proof

pf

Apply unknownprop_d378b2c894939b96acaefeb7b90d3a62ba779e2a2ea4390f7801c59b07291ce2 with λ x0 . True leaving 2 subgoals.

Let x0 of type ι be given.

Assume H0: True.

Let x1 of type ι be given.

Assume H1: True.

The subproof is completed by applying TrueI.

Let x0 of type ι be given.

Assume H0: True.

Let x1 of type ι be given.

Assume H1: True.

The subproof is completed by applying TrueI.

■