| ∀ x0 x1 . nat_p x0 ⟶ ∀ x2 : ι → ι . ∀ x3 x4 x5 x6 . nat_p x3 ⟶ nat_p x4 ⟶ (x3 = x4 ⟶ ∀ x7 : ο . x7) ⟶ nat_p x5 ⟶ nat_p x6 ⟶ (∀ x7 . x7 ∈ x0 ⟶ x2 x7 ∈ x1) ⟶ (∀ x7 . x7 ∈ x1 ⟶ or (equip {x8 ∈ x0|x2 x8 = x7} x3) (equip {x8 ∈ x0|x2 x8 = x7} x4)) ⟶ equip {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x3} x5 ⟶ equip {x7 ∈ x1|equip {x8 ∈ x0|x2 x8 = x7} x4} x6 ⟶ add_nat (mul_nat x5 x3) (mul_nat x6 x4) = x0 |
|