Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: and (TransSet x0) (∀ x1 . prim1 x1 x0 ⟶ TransSet x1).
Let x1 of type ι be given.
Assume H1: prim1 x1 x0.
Apply H0 with and (TransSet x1) (∀ x2 . prim1 x2 x1 ⟶ TransSet x2).
Assume H2: TransSet x0.
Assume H3: ∀ x2 . prim1 x2 x0 ⟶ TransSet x2.
Apply andI with TransSet x1, ∀ x2 . prim1 x2 x1 ⟶ TransSet x2 leaving 2 subgoals.
Apply H3 with x1.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H4: prim1 x2 x1.
Claim L5: prim1 x2 x0
Apply H2 with x1, x2 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
Apply H3 with x2.
The subproof is completed by applying L5.
■