Proofgold Proof

pf

Let x0 of type ο be given.

Let x1 of type ο be given.

Assume H0: not x0 ⟶ x1.

Assume H1: not x1.

Apply unknownprop_b777a79c17f16cd28153af063df26a4626b11c1f1d4394d7f537c11837ab0962 with x0.

Assume H2: not x0.

Apply notE with not x1 leaving 2 subgoals.

set y2 to be x1

Claim L3: y2

Apply H0.

The subproof is completed by applying H2.

Apply unknownprop_e284d5f5a7c3a1c03631041619c4ddee06de72330506f5f6d9d6b18df929e48c with not y2.

Assume H4: not y2.

Apply notE with y2 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying L3.

The subproof is completed by applying H1.

■