Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_1784a2340ad00d1f56caafe40e76ea8159b7d6bc0008eed82e9e91210d8ef647 with
x0,
x1,
λ x2 x3 . prim1 x2 48ef8.. leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_b67f6d586fb9d8883c38540f89ba210beeb3fabc8048f066af6580d3cbff51ec with
616bf.. x0 x1.
Apply unknownprop_6ea59642454c806d36d2cfe931420377c027fcaf6c044cc84fb5291b346de8a0 with
x0,
x1 leaving 2 subgoals.
Apply unknownprop_03f5f7248b8d06fe27b9a4f75f4e437d5e9b43a9092733e8b3f6dcfe61f5e308 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_03f5f7248b8d06fe27b9a4f75f4e437d5e9b43a9092733e8b3f6dcfe61f5e308 with
x1.
The subproof is completed by applying H1.