Let x0 of type ι be given.
Let x1 of type ι be given.
Apply set_ext with
x0,
x1 leaving 2 subgoals.
Apply unknownprop_258858c3050447844332df7e4e4b4146507256ca0e8d596f8d7d17cb469d4a54 with
x0,
x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply H2 with
λ x2 x3 . Subq (e4431.. x0) x2.
The subproof is completed by applying Subq_ref with
e4431.. x0.
The subproof is completed by applying H3.
Apply unknownprop_258858c3050447844332df7e4e4b4146507256ca0e8d596f8d7d17cb469d4a54 with
x1,
x0 leaving 4 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply H2 with
λ x2 x3 . Subq (e4431.. x1) x3.
The subproof is completed by applying Subq_ref with
e4431.. x1.
Let x2 of type ι be given.
Apply iff_sym with
prim1 x2 x0,
prim1 x2 x1.
Apply H3 with
x2.
Apply H2 with
λ x3 x4 . prim1 x2 x4.
The subproof is completed by applying H4.