Search for blocks/addresses/...

Proofgold Proof

pf
Apply unknownprop_acac0f89c78f08b97a9fe27ba4af5f929f74e43a9a77a0beb38d70975279c8b8 with λ x0 . Unj (Inj1 x0) = x0.
Let x0 of type ι be given.
Assume H0: ∀ x1 . In x1 x0Unj (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.
Assume H1: In x1 (Repl (setminus (Inj1 x0) (Sing 0)) (λ x2 . Unj x2)).
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.
Assume H2: In x2 (setminus (Inj1 x0) (Sing 0)).
Assume H3: x1 = Unj x2.
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.
Assume H4: In x2 (Inj1 x0).
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.
Assume H5: nIn 0 (Sing 0).
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.
Assume H5: In x3 x0.
Assume H6: nIn (Inj1 x3) (Sing 0).
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.
Assume H1: In x1 x0.
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.