Coq: Доказательство предложения f (xy) -> fy

Question

Можно ли доказать

Lemma A3 (f x: Prop -> Prop)(y: Prop): f (x y) -> f y.

либо с / или (предпочтительно) с / без аксиом?

Answer 1

Ответ "нет" на доказательство без аксиом (и я боюсь, что может быть трудно найти значимые аксиомы для доказательства этого также).Предположим, что

Parameter A3: forall (f x:Prop->Prop)(y:Prop), f (x y) -> f y.
Definition f' (x:Prop) := x.
Definition X := fun _:Prop => True.
Check A3 f' X False: True -> False.

A3 f' X False имеет тип True -> False, что недоказуемо