Let x0 of type ι be given.
Apply nat_ind with
λ x1 . equip (exp_nat x0 x1) (setexp x0 x1) leaving 2 subgoals.
Apply unknownprop_e320081fa46c313032b82ae65d08f162063eec597356adc2ef96e4883b8d3302 with
x0,
λ x1 x2 . equip x2 (setexp x0 0).
Apply equip_sym with
setexp x0 0,
1.
The subproof is completed by applying unknownprop_62fa75c17c3e844b21d255650e97642a49307dfdd0dcd86f1d15a71f14f047cb with x0.
Let x1 of type ι be given.
Apply equip_sym with
exp_nat x0 x1,
setexp x0 x1,
equip (exp_nat x0 (ordsucc x1)) (setexp x0 (ordsucc x1)) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ι → ι be given.
Apply H3 with
equip (exp_nat x0 (ordsucc x1)) (setexp x0 (ordsucc x1)).
Assume H4:
and (∀ x3 . x3 ∈ setexp x0 x1 ⟶ x2 x3 ∈ exp_nat x0 x1) (∀ x3 . x3 ∈ setexp x0 x1 ⟶ ∀ x4 . x4 ∈ setexp x0 x1 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4).
Apply H4 with
(∀ x3 . x3 ∈ exp_nat x0 x1 ⟶ ∃ x4 . and (x4 ∈ setexp x0 x1) (x2 x4 = x3)) ⟶ equip (exp_nat x0 (ordsucc x1)) (setexp x0 (ordsucc x1)).
Assume H6:
∀ x3 . x3 ∈ setexp x0 x1 ⟶ ∀ x4 . x4 ∈ setexp x0 x1 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.
Assume H7:
∀ x3 . x3 ∈ exp_nat x0 x1 ⟶ ∃ x4 . and (x4 ∈ setexp x0 x1) (x2 x4 = x3).
Apply unknownprop_e9c4cec7fb327dcb17b88acdaf76daee024e49fa71834a13065f86e12e958609 with
x0,
x1,
λ x3 x4 . equip x4 (setexp x0 (ordsucc x1)) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply equip_tra with
mul_nat x0 (exp_nat x0 x1),
setprod x0 (exp_nat x0 x1),
setexp x0 (ordsucc x1) leaving 2 subgoals.
Apply unknownprop_b67c3f99b7dcb350283e28e0205622aac5c4480ca587d55b1fc9b439a7a164e1 with
x0,
exp_nat x0 x1,
x0,
exp_nat x0 x1 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_1b73e01bc234ba0e318bc9baf16604d4f0fc12bea57885439d70438de4eb7174 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying equip_ref with x0.
The subproof is completed by applying equip_ref with
exp_nat x0 x1.