| pf |
|---|
Apply unknownprop_a3891bc0c376c56135af0ba3023ea81094f615683f2cdf7844968055e83fedae with 0, 1, Sing 1, Sing 2, 2, UPair 0 2, UPair 1 2, 3, prim4 3 leaving 29 subgoals.
Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Assume H1: x1 0.
Assume H2: x1 1.
Assume H5: x1 2.
Assume H6: x1 (UPair 0 2). Assume H7: x1 (UPair 1 2). Assume H8: x1 3.
Apply In_Power_3_cases_impred with x0, x1 x0 leaving 9 subgoals.
The subproof is completed by applying H0.
Assume H9: x0 = 0.
Apply H9 with λ x2 x3 . x1 x3.
The subproof is completed by applying H1.
Assume H9: x0 = 1.
Apply H9 with λ x2 x3 . x1 x3.
The subproof is completed by applying H2.
Apply H9 with λ x2 x3 . x1 x3.
The subproof is completed by applying H3.
Assume H9: x0 = 2.
Apply H9 with λ x2 x3 . x1 x3.
The subproof is completed by applying H5.
Apply H9 with λ x2 x3 . x1 x3.
The subproof is completed by applying H4.
Assume H9: x0 = UPair 0 2. Apply H9 with λ x2 x3 . x1 x3.
The subproof is completed by applying H6.
Assume H9: x0 = UPair 1 2. Apply H9 with λ x2 x3 . x1 x3.
The subproof is completed by applying H7.
Assume H9: x0 = 3.
Apply H9 with λ x2 x3 . x1 x3.
The subproof is completed by applying H8.
The subproof is completed by applying neq_0_1.
The subproof is completed by applying not_Empty_eq_Sing with 1.
Apply nIn_not_eq_Sing with 1, 1.
The subproof is completed by applying In_irref with 1.
The subproof is completed by applying not_Empty_eq_Sing with 2.
Apply nIn_not_eq_Sing with 2, 1.
The subproof is completed by applying nIn_2_1.
Apply nIn_not_eq_Sing with 2, Sing 1.
Apply neq_2_1.
Apply SingE with 1, 2.
The subproof is completed by applying H0.
The subproof is completed by applying neq_0_2.
The subproof is completed by applying neq_1_2.
Apply neq_0_1.
Apply SingE with 1, 0.
Apply H0 with λ x0 x1 . 0 ∈ x1.
The subproof is completed by applying In_0_2.
Apply neq_i_sym with 2, Sing 2.
Apply nIn_not_eq_Sing with 2, 2.
The subproof is completed by applying In_irref with 2.
The subproof is completed by applying not_Empty_eq_UPair with 0, 2.
Apply nIn_not_eq_UPair_2 with 0, 2, 1.
The subproof is completed by applying nIn_2_1.
Apply nIn_not_eq_UPair_1 with 0, 2, Sing 1.
Apply neq_0_1.
Apply SingE with 1, 0.
The subproof is completed by applying H0.
Apply nIn_not_eq_UPair_1 with 0, 2, Sing 2.
Apply neq_0_2.
Apply SingE with 2, 0.
The subproof is completed by applying H0.
Apply nIn_not_eq_UPair_2 with 0, 2, 2.
The subproof is completed by applying In_irref with 2.
The subproof is completed by applying not_Empty_eq_UPair with 1, 2.
Apply nIn_not_eq_UPair_2 with 1, 2, 1.
The subproof is completed by applying nIn_2_1.
Apply nIn_not_eq_UPair_2 with 1, 2, Sing 1.
Apply neq_2_1.
Apply SingE with 1, 2.
The subproof is completed by applying H0.
Apply nIn_not_eq_UPair_1 with 1, 2, Sing 2.
Apply neq_1_2.
Apply SingE with 2, 1.
The subproof is completed by applying H0.
Apply nIn_not_eq_UPair_2 with 1, 2, 2.
The subproof is completed by applying In_irref with 2.
Apply nIn_not_eq_UPair_1 with 1, 2, UPair 0 2.
Assume H0: 1 ∈ UPair 0 2. Apply UPairE with 1, 0, 2, False leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying neq_1_0.
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_0_1.
Apply SingE with 1, 0.
Apply H0 with λ x0 x1 . 0 ∈ x1.
The subproof is completed by applying In_0_3.
Apply neq_0_2.
Apply SingE with 2, 0.
Apply H0 with λ x0 x1 . 0 ∈ x1.
The subproof is completed by applying In_0_3.
Apply neq_i_sym with 3, 2.
The subproof is completed by applying neq_3_2.
Assume H0: UPair 0 2 = 3. Apply UPairE with 1, 0, 2, False leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying neq_1_0.
The subproof is completed by applying neq_1_2.
■ |
|