Let x0 of type ι be given.
Let x1 of type ι be given.
Apply prop_ext_2 with
Subq x0 x1,
binunion x0 x1 = x1 leaving 2 subgoals.
Apply unknownprop_a23ec6a55ac212526d74cbf0d04096929ad453b0eb0f8023e32b8a33930d39fb with
binunion x0 x1,
x1 leaving 2 subgoals.
Apply unknownprop_fb26fe958e64ebbf533947db0048c8f1c2bfe1ee93c5358b327221e99f81f109 with
x0,
x1,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_d889823a5c975ad2d68f484964233a1e69e7d67f0888aa5b83d962eeca107acd with x1.
The subproof is completed by applying unknownprop_797168717b55ee5eded5eab45e11f1513074138c4f7a9fa70fbdac8b84ce4a03 with x0, x1.
Apply H0 with
λ x2 x3 . Subq x0 x2.
The subproof is completed by applying unknownprop_45cad3d16e6a052331516a33ff7f695a27568e6c7992c9bc7ae67399a451422e with x0, x1.