| pf |
|---|
Apply unknownprop_a3891bc0c376c56135af0ba3023ea81094f615683f2cdf7844968055e83fedae with 0, 1, 2, 3, 4, 5, 6, 7, 8 leaving 30 subgoals.
The subproof is completed by applying cases_8.
The subproof is completed by applying neq_0_1.
The subproof is completed by applying neq_0_2.
The subproof is completed by applying neq_1_2.
Apply neq_i_sym with 3, 0.
The subproof is completed by applying neq_3_0.
Apply neq_i_sym with 3, 1.
The subproof is completed by applying neq_3_1.
Apply neq_i_sym with 3, 2.
The subproof is completed by applying neq_3_2.
Apply neq_i_sym with 4, 0.
The subproof is completed by applying neq_4_0.
Apply neq_i_sym with 4, 1.
The subproof is completed by applying neq_4_1.
Apply neq_i_sym with 4, 2.
The subproof is completed by applying neq_4_2.
Apply neq_i_sym with 4, 3.
The subproof is completed by applying neq_4_3.
Apply neq_i_sym with 5, 0.
The subproof is completed by applying neq_5_0.
Apply neq_i_sym with 5, 1.
The subproof is completed by applying neq_5_1.
Apply neq_i_sym with 5, 2.
The subproof is completed by applying neq_5_2.
Apply neq_i_sym with 5, 3.
The subproof is completed by applying neq_5_3.
Apply neq_i_sym with 5, 4.
The subproof is completed by applying neq_5_4.
Apply neq_i_sym with 6, 0.
The subproof is completed by applying neq_6_0.
Apply neq_i_sym with 6, 1.
The subproof is completed by applying neq_6_1.
Apply neq_i_sym with 6, 2.
The subproof is completed by applying neq_6_2.
Apply neq_i_sym with 6, 3.
The subproof is completed by applying neq_6_3.
Apply neq_i_sym with 6, 4.
The subproof is completed by applying neq_6_4.
Apply neq_i_sym with 6, 5.
The subproof is completed by applying neq_6_5.
Apply neq_i_sym with 7, 0.
The subproof is completed by applying neq_7_0.
Apply neq_i_sym with 7, 1.
The subproof is completed by applying neq_7_1.
Apply neq_i_sym with 7, 2.
The subproof is completed by applying neq_7_2.
Apply neq_i_sym with 7, 3.
The subproof is completed by applying neq_7_3.
Apply neq_i_sym with 7, 4.
The subproof is completed by applying neq_7_4.
Apply neq_i_sym with 7, 5.
The subproof is completed by applying neq_7_5.
Apply neq_i_sym with 7, 6.
The subproof is completed by applying neq_7_6.
Apply TwoRamseyProp_atleastp_atleastp with 3, 3, 4, 4, 8 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying atleastp_ref with 3.
The subproof is completed by applying atleastp_ref with 4.
■ |
|