Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
Repl x0 (λ x2 . x1 x2),
famunion x0 (λ x2 . Sing (x1 x2)) leaving 2 subgoals.
Let x2 of type ι be given.
Assume H0:
In x2 (Repl x0 (λ x3 . x1 x3)).
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with
x0,
x1,
x2,
In x2 (famunion x0 (λ x3 . Sing (x1 x3))) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H2: x2 = x1 x3.
Apply unknownprop_4d9a081a15fdc79c67eee9fe67650a775bc97737c16f9cc2a1a6fdd7a2cc8108 with
x0,
λ x4 . Sing (x1 x4),
x3,
x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply H2 with
λ x4 x5 . In x2 (Sing x4).
The subproof is completed by applying unknownprop_e96dbc98c3bbaccd959c44021711d14fb0c42be8979571d40cfb87c8bcb73964 with x2.
Let x2 of type ι be given.
Apply unknownprop_a7f2dda18b84bce65b5de34328a937fef2c23812675d88bde1e7e2463ed59bbe with
x0,
λ x3 . Sing (x1 x3),
x2,
In x2 (Repl x0 (λ x3 . x1 x3)) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ι be given.
Assume H2:
In x2 (Sing (x1 x3)).
Claim L3: x2 = x1 x3
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
x1 x3,
x2.
The subproof is completed by applying H2.
Apply L3 with
λ x4 x5 . In x5 (Repl x0 (λ x6 . x1 x6)).
Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with
x0,
x1,
x3.
The subproof is completed by applying H1.