| pf |
|---|
Apply nat_ind with λ x0 . ∀ x1 . equip x1 x0 ⟶ equip (prim4 x1) (exp_nat 2 x0) leaving 2 subgoals.
Let x0 of type ι be given.
Apply equip_0_Empty with x0, λ x1 x2 . equip (prim4 x2) (exp_nat 2 0) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_e320081fa46c313032b82ae65d08f162063eec597356adc2ef96e4883b8d3302 with 2, λ x1 x2 . equip (prim4 0) x2.
Apply Power_0_Sing_0 with λ x1 x2 . equip x2 1.
Apply eq_1_Sing0 with λ x1 x2 . equip x1 1.
The subproof is completed by applying equip_ref with 1.
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_e9c4cec7fb327dcb17b88acdaf76daee024e49fa71834a13065f86e12e958609 with 2, x0, λ x2 x3 . equip (prim4 x1) x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply mul_nat_com with 2, exp_nat 2 x0, λ x2 x3 . equip (prim4 x1) x3 leaving 3 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying L3.
Apply add_nat_1_1_2 with λ x2 x3 . equip (prim4 x1) (mul_nat (exp_nat 2 x0) x2).
Apply mul_add_nat_distrL with exp_nat 2 x0, 1, 1, λ x2 x3 . equip (prim4 x1) x3 leaving 4 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying nat_1.
The subproof is completed by applying nat_1.
Apply mul_nat_1R with exp_nat 2 x0, λ x2 x3 . equip (prim4 x1) (add_nat x3 x3).
Apply equip_sym with x1, ordsucc x0, ∃ x2 . x2 ∈ x1, equip (prim4 x1) (add_nat (exp_nat 2 x0) (exp_nat 2 x0)) leaving 3 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι → ι be given.
Apply H4 with ∃ x3 . x3 ∈ x1.
Assume H5: and (∀ x3 . x3 ∈ ordsucc x0 ⟶ x2 x3 ∈ x1) (∀ x3 . x3 ∈ ordsucc x0 ⟶ ∀ x4 . x4 ∈ ordsucc x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4). Assume H6: ∀ x3 . x3 ∈ x1 ⟶ ∃ x4 . and (x4 ∈ ordsucc x0) (x2 x4 = x3). Apply H5 with ∃ x3 . x3 ∈ x1.
Assume H7: ∀ x3 . x3 ∈ ordsucc x0 ⟶ x2 x3 ∈ x1. Assume H8: ∀ x3 . x3 ∈ ordsucc x0 ⟶ ∀ x4 . x4 ∈ ordsucc x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4. Let x3 of type ο be given.
Assume H9: ∀ x4 . x4 ∈ x1 ⟶ x3.
Apply H9 with x2 x0.
Apply H7 with x0.
The subproof is completed by applying ordsuccI2 with x0.
Let x2 of type ι be given.
Assume H4: (λ x3 . x3 ∈ x1) x2.
Apply H1 with setminus x1 (Sing x2), equip (prim4 x1) (add_nat (exp_nat 2 x0) (exp_nat 2 x0)) leaving 2 subgoals.
Apply unknownprop_997b324045b1165b0cf38788927ff324ddb3a505c8b91e290586e4dd5480f2bd with x1, x0, x2 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H2.
Let x3 of type ι → ι be given.
■ |
|