In z_app_thm, which states ∀ a : 𝕌; f : 𝕌; x : 𝕌 ⦁ (∀ f_a : 𝕌 | (a, f_a) ∈ f ⦁ f_a = x) ∧ (a, x) ∈ f ⇒ f a = x

## Advertising

I notice that the antecedent (a, x) ∈ f

`does not actually need to map a to x because that is already captured in`

`the first antecedent. It only needs to say that a is in the domain of`

`f, so the theorem could state`

∀ a : 𝕌; f : 𝕌; x, y : 𝕌 ⦁ (∀ f_a : 𝕌 | (a, f_a) ∈ f ⦁ f_a = x) ∧ (a, y) ∈ f ⇒ f a = x

`As it stands, I suspect there could be some unnecessary proof overhead`

`for users (and perhaps in the PP implementation) because it may be`

`necessary to forward chain with the left antecedent, once established,`

`and eliminate a variable to get the form required by z_app_thm.`

`I think other proof operations like z_app_eq_tac and z_app_λ_rule would`

`naturally become simpler:`

- z_app_eq_tac could return a goal containing ... ∧ (∃ v : 𝕌 ⦁ (a, v) ∈ f) so we can choose any v, instead of ... ∧ (a, v) ∈ f - z_app_λ_rule would not include the predicate V' = x in the antecedents. Phil _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com