Apply unknownprop_acac0f89c78f08b97a9fe27ba4af5f929f74e43a9a77a0beb38d70975279c8b8 with
λ x0 . Unj (Inj1 x0) = x0.
Let x0 of type ι be given.
Assume H0:
∀ x1 . In x1 x0 ⟶ Unj (Inj1 x1) = x1.
Apply unknownprop_90bc64785a62f436436f79ffade2005019961924ea270765e5e2c87d9af3394c with
Inj1 x0,
λ x1 x2 . x2 = x0.
Apply unknownprop_219a5692ece616b4a88502d80a85b644180cde982b21251f92a23d11d1a5d022 with
Repl (setminus (Inj1 x0) (Sing 0)) (λ x1 . Unj x1),
x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_89e422bb3b8a01dd209d7f2f210df650a435fc3e6005e0f59c57a5e7a59a6d0e with
setminus (Inj1 x0) (Sing 0),
Unj,
x1,
In x1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply H3 with
λ x3 x4 . In x4 x0.
Apply unknownprop_e02b92c94ff70655b8eb0623a7ec106c0c0c9c65ac0f52f9689f2e6c9f563b5d with
Inj1 x0,
Sing 0,
x2,
In (Unj x2) x0 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_0b120035bc22426ea02988561990499be78ef89e658ec0c0b4bcff54639930cb with
x0,
x2,
λ x3 . nIn x3 (Sing 0) ⟶ In (Unj x3) x0 leaving 3 subgoals.
The subproof is completed by applying H4.
Apply FalseE with
In (Unj 0) x0.
Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with
0,
Sing 0 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying unknownprop_e96dbc98c3bbaccd959c44021711d14fb0c42be8979571d40cfb87c8bcb73964 with 0.
Let x3 of type ι be given.
Apply H0 with
x3,
λ x4 x5 . In x5 x0 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Apply H0 with
x1,
λ x2 x3 . In x2 (Repl (setminus (Inj1 x0) (Sing 0)) (λ x4 . Unj x4)) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_63c308b92260dbfca8c9530846e6836ba3e6be221cc8e80fd61db913e01bdacf with
setminus (Inj1 x0) (Sing 0),
Unj,
Inj1 x1.
Apply unknownprop_3fe7f97dcb00bcf31cf989081bd8403f8f0647acc7dd719f8a7da64cd4837dac with
Inj1 x0,
Sing 0,
Inj1 x1 leaving 2 subgoals.
Apply unknownprop_20467f36510c7b6830c7e44d6955dc079b6e83b8bbc05b0500ccb9075a391641 with
x0,
x1.
The subproof is completed by applying H1.
The subproof is completed by applying unknownprop_19d5e1f06b8ff33ed1f0a1ec773eb4ad1cafb04cacdc9f1d5ac58ef21224c105 with x1.