Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_73b6444bcb1b9cb998566f55e286e78644e785a99d955b3281cf269899ab486c with
e4431.. x0,
e4431.. x1,
λ x2 . prim1 x2 x0,
λ x2 . prim1 x2 x1,
or (or (099f3.. x0 x1) (x0 = x1)) (099f3.. x1 x0) leaving 4 subgoals.
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_afbf697e4489c80654ae2bc4c6605f6f1d2a8b7dcfe3f07863a96592ab5c88f5 with
x1.
The subproof is completed by applying H1.
Apply H2 with
or (or (099f3.. x0 x1) (x0 = x1)) (099f3.. x1 x0) leaving 2 subgoals.
Apply or3I1 with
099f3.. x0 x1,
x0 = x1,
099f3.. x1 x0.
The subproof is completed by applying H3.
Apply H3 with
or (or (099f3.. x0 x1) (x0 = x1)) (099f3.. x1 x0).
Apply or3I2 with
099f3.. x0 x1,
x0 = x1,
099f3.. x1 x0.
Apply unknownprop_c3102c186c7aa1001a5c1b1b7ecab6b25bcd639e713104221ece8bf414726a69 with
x0,
x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply or3I3 with
099f3.. x0 x1,
x0 = x1,
099f3.. x1 x0.
The subproof is completed by applying H2.