| pf |
|---|
Apply bijI with u3, {x0 ∈ prim4 u3|equip x0 u2}, λ x0 . ap (lam 3 (λ x1 . If_i (x1 = 0) (UPair 0 u1) (If_i (x1 = 1) (UPair 0 u2) (UPair u1 u2)))) x0 leaving 3 subgoals.
Let x0 of type ι be given.
Apply cases_3 with x0, λ x1 . ap (lam 3 (λ x2 . If_i (x2 = 0) (UPair 0 u1) (If_i (x2 = 1) (UPair 0 u2) (UPair u1 u2)))) x1 ∈ {x2 ∈ prim4 u3|equip x2 u2} leaving 4 subgoals.
The subproof is completed by applying H1.
Apply tuple_3_0_eq with UPair 0 u1, UPair 0 u2, UPair u1 u2, λ x1 x2 . x2 ∈ {x3 ∈ prim4 u3|equip x3 u2}.
Apply SepI with prim4 u3, λ x1 . equip x1 u2, UPair 0 u1 leaving 2 subgoals.
Apply PowerI with u3, UPair 0 u1.
Let x1 of type ι be given.
Apply UPairE with x1, 0, u1, x1 ∈ u3 leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: x1 = 0.
Apply H3 with λ x2 x3 . x3 ∈ u3.
The subproof is completed by applying In_0_3.
Apply H3 with λ x2 x3 . x3 ∈ u3.
The subproof is completed by applying In_1_3.
Apply unknownprop_39df499f773ced696ac600b0767cd28b9ceea72e50ff2c9103bc16896281c585 with 0, u1.
The subproof is completed by applying neq_0_1.
Apply tuple_3_1_eq with UPair 0 u1, UPair 0 u2, UPair u1 u2, λ x1 x2 . x2 ∈ {x3 ∈ prim4 u3|equip x3 u2}.
Apply SepI with prim4 u3, λ x1 . equip x1 u2, UPair 0 u2 leaving 2 subgoals.
Apply PowerI with u3, UPair 0 u2.
Let x1 of type ι be given.
Apply UPairE with x1, 0, u2, x1 ∈ u3 leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: x1 = 0.
Apply H3 with λ x2 x3 . x3 ∈ u3.
The subproof is completed by applying In_0_3.
Apply H3 with λ x2 x3 . x3 ∈ u3.
The subproof is completed by applying In_2_3.
Apply unknownprop_39df499f773ced696ac600b0767cd28b9ceea72e50ff2c9103bc16896281c585 with 0, u2.
The subproof is completed by applying neq_0_2.
Apply tuple_3_2_eq with UPair 0 u1, UPair 0 u2, UPair u1 u2, λ x1 x2 . x2 ∈ {x3 ∈ prim4 u3|equip x3 u2}.
Apply SepI with prim4 u3, λ x1 . equip x1 u2, UPair u1 u2 leaving 2 subgoals.
Apply PowerI with u3, UPair u1 u2.
Let x1 of type ι be given.
Apply UPairE with x1, u1, u2, x1 ∈ u3 leaving 3 subgoals.
The subproof is completed by applying H2.
Apply H3 with λ x2 x3 . x3 ∈ u3.
The subproof is completed by applying In_1_3.
Apply H3 with λ x2 x3 . x3 ∈ u3.
The subproof is completed by applying In_2_3.
Apply unknownprop_39df499f773ced696ac600b0767cd28b9ceea72e50ff2c9103bc16896281c585 with u1, u2.
The subproof is completed by applying neq_1_2.
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply cases_3 with x0, λ x2 . (λ x3 . ap (lam 3 (λ x4 . If_i (x4 = 0) (UPair 0 u1) (If_i (x4 = 1) ... ...))) ...) ... = ... ⟶ x2 = x1 leaving 4 subgoals.
■ |
|