Let x0 of type ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
Union x0,
famunion x0 (λ x1 . x1) leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_99c6830b7507eb1c538c7366f637e956be6dad337531dd2702ca6ba6923a9849 with
x0,
x1,
In x1 (famunion x0 (λ x2 . x2)) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply unknownprop_4d9a081a15fdc79c67eee9fe67650a775bc97737c16f9cc2a1a6fdd7a2cc8108 with
x0,
λ x3 . x3,
x2,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply unknownprop_a7f2dda18b84bce65b5de34328a937fef2c23812675d88bde1e7e2463ed59bbe with
x0,
λ x2 . x2,
x1,
In x1 (Union x0) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι be given.
Apply unknownprop_bb7319fda7123d5f775b6b29aaea60dee8b8450dbda3fb13de42ee7deaa111d5 with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.