Let x0 of type ι be given.
Let x1 of type ι be given.
Apply andI with
prim1 x0 x1,
∀ x2 . prim1 x2 x1 ⟶ x2 = x0 leaving 2 subgoals.
Apply H0 with
λ x2 x3 . prim1 x0 x2.
The subproof is completed by applying unknownprop_c6d721b795faf1c324094ad380dfe62a3a5dc2ef0b2edf42237be188f6768728 with x0.
Let x2 of type ι be given.
Apply H0 with
λ x3 x4 . prim1 x2 x3 ⟶ x2 = x0.
Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with
x0,
x2.
The subproof is completed by applying H1.