Let x0 of type ι → ο be given.
Let x1 of type ι → ι be given.
Let x2 of type ο be given.
Apply H0 with
0.
Let x3 of type ι be given.
Apply H1 with
∃ x4 . and (and (x0 0) (x0 x3)) (reflexive_i (λ x5 x6 . x0 x5) ⟶ and (x0 0) (and (x0 (x1 x3)) (not (atleast6 x4)))).
Let x4 of type ι be given.
Apply andE with
exactly3 0,
not (x0 x3),
∃ x5 . and (and (x0 0) (x0 x3)) (reflexive_i (λ x6 x7 . x0 x6) ⟶ and (x0 0) (and (x0 (x1 x3)) (not (atleast6 x5)))) leaving 2 subgoals.
The subproof is completed by applying H2.
Apply FalseE with
not (x0 x3) ⟶ ∃ x5 . and (and (x0 0) (x0 x3)) (reflexive_i (λ x6 x7 . x0 x6) ⟶ and (x0 0) (and (x0 (x1 x3)) (not (atleast6 x5)))).
Apply unknownprop_c29e201c2636d12615b11e1220001fcc0c2bbdeb53735eb34683c60a05a28860 with
atleast3 0,
not (atleast4 0).
Apply unknownprop_c9103b15101bbc1f738ceaf0919de1c89b5c7611420a12711eed9f8143f9b582 with
0.
The subproof is completed by applying H3.
Apply unknownprop_8ba3cc049a46be464fc77cd637cbc117a0f7ace4cdc85587acac7999a5948772 with
0,
False leaving 2 subgoals.
The subproof is completed by applying L4.
Let x5 of type ι be given.
Apply andE with
Subq x5 0,
and (not (Subq 0 x5)) (atleast2 x5),
False leaving 2 subgoals.
The subproof is completed by applying H5.
Apply notE with
Subq 0 x5 leaving 2 subgoals.
Apply unknownprop_c29e201c2636d12615b11e1220001fcc0c2bbdeb53735eb34683c60a05a28860 with
not (Subq 0 x5),
atleast2 x5.
The subproof is completed by applying H7.
The subproof is completed by applying unknownprop_48b433c7921d49bb7e4205d5d86f68a84030c1b7df98f7a59f08a308cb665298 with x5.