Let x0 of type ι be given.
Let x1 of type ι be given.
Apply and6I with
90aea.. x0,
90aea.. x1,
90aea.. (pack_r 0 (λ x2 x3 . False)),
BinRelnHom (pack_r 0 (λ x2 x3 . False)) x0 0,
BinRelnHom (pack_r 0 (λ x2 x3 . False)) x1 0,
∀ x2 . 90aea.. x2 ⟶ ∀ x3 x4 . BinRelnHom x2 x0 x3 ⟶ BinRelnHom x2 x1 x4 ⟶ and (and (and (BinRelnHom x2 (pack_r 0 (λ x5 x6 . False)) 0) (struct_comp x2 (pack_r 0 (λ x5 x6 . False)) x0 0 0 = x3)) (struct_comp x2 (pack_r 0 (λ x5 x6 . False)) x1 0 0 = x4)) (∀ x5 . BinRelnHom x2 (pack_r 0 (λ x6 x7 . False)) x5 ⟶ struct_comp x2 (pack_r 0 (λ x6 x7 . False)) x0 0 x5 = x3 ⟶ struct_comp x2 (pack_r 0 (λ x6 x7 . False)) x1 0 x5 = x4 ⟶ x5 = 0) leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying L2.
Apply unknownprop_db29be70f626d907819defaaafb0849de7b3b2be132ffdec2cf3d6bf6e7f756a with
pack_r 0 (λ x2 x3 . False),
x0 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H0.
Apply unknownprop_db29be70f626d907819defaaafb0849de7b3b2be132ffdec2cf3d6bf6e7f756a with
pack_r 0 (λ x2 x3 . False),
x1 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply and4I with
BinRelnHom x2 (pack_r 0 (λ x5 x6 . False)) 0,
struct_comp x2 (pack_r 0 (λ x5 x6 . False)) x0 0 0 = x3,
struct_comp x2 (pack_r 0 (λ x5 x6 . False)) x1 0 0 = x4,
∀ x5 . BinRelnHom x2 (pack_r 0 (λ x6 x7 . False)) x5 ⟶ struct_comp x2 (pack_r 0 (λ x6 x7 . False)) x0 0 x5 = x3 ⟶ struct_comp x2 (pack_r 0 (λ x6 x7 . False)) x1 0 x5 = x4 ⟶ x5 = 0 leaving 4 subgoals.
Apply unknownprop_db29be70f626d907819defaaafb0849de7b3b2be132ffdec2cf3d6bf6e7f756a with
x2,
pack_r 0 (λ x5 x6 . False) leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L2.
Apply L6 with
λ x5 x6 . struct_comp x2 (pack_r 0 (λ x7 x8 . False)) x0 0 0 = x6.
Apply unknownprop_765d413c5d1a8be896fb2d38fda75f9803185335550bf0cbde813c254ddda463 with
x2,
pack_r 0 (λ x5 x6 . False),
x0,
0,
0.
The subproof is completed by applying H3.
Apply L7 with
λ x5 x6 . struct_comp x2 (pack_r 0 (λ x7 x8 . False)) x1 0 0 = x6.
Apply unknownprop_765d413c5d1a8be896fb2d38fda75f9803185335550bf0cbde813c254ddda463 with
x2,
pack_r 0 (λ x5 x6 . False),
x1,
0,
0.
The subproof is completed by applying H3.
Let x5 of type ι be given.