| pf |
|---|
Apply andI with 90aea.. (pack_r 0 (λ x0 x1 . False)), ∀ x0 . 90aea.. x0 ⟶ and (BinRelnHom x0 (pack_r 0 (λ x1 x2 . False)) 0) (∀ x1 . BinRelnHom x0 (pack_r 0 (λ x2 x3 . False)) x1 ⟶ x1 = 0) leaving 2 subgoals.
The subproof is completed by applying unknownprop_368e92f67c0383aee9043344ceeddddb8cd4a69474da241bb811d114c3a8b2be.
Let x0 of type ι be given.
Apply unknownprop_589446c7eb1e0f49f9a1c9ecf95332e51a36bcf398bd883c8295d2920f123b6b with x0, pack_r 0 (λ x1 x2 . False), 0, λ x1 x2 : ο . and x2 (∀ x3 . BinRelnHom x0 (pack_r 0 (λ x4 x5 . False)) x3 ⟶ x3 = 0) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_368e92f67c0383aee9043344ceeddddb8cd4a69474da241bb811d114c3a8b2be.
Apply andI with 0 = 0, ∀ x1 . BinRelnHom x0 (pack_r 0 (λ x2 x3 . False)) x1 ⟶ x1 = 0 leaving 2 subgoals.
Let x1 of type ι → ι → ο be given.
Assume H1: x1 0 0.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply unknownprop_589446c7eb1e0f49f9a1c9ecf95332e51a36bcf398bd883c8295d2920f123b6b with x0, pack_r 0 (λ x2 x3 . False), x1, λ x2 x3 : ο . x3 ⟶ x1 = 0 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_368e92f67c0383aee9043344ceeddddb8cd4a69474da241bb811d114c3a8b2be.
Assume H1: x1 = 0.
The subproof is completed by applying H1.
■ |
|