Crowdly
Додати до Chrome
Observe the following Lean code: example : (∃ x : A, PP x) → (∀ y : A, PP...
✅ Перевірена відповідь на це питання доступна нижче. Наші рішення, перевірені спільнотою, допомагають краще зрозуміти матеріал.
Observe the following Lean code:
example : (∃ x : A, PP x) → (∀ y : A, PP y → QQ y) → ∃ z : A , QQ z :=
begin
assume p pq,
cases p with a pa,
sorry,
apply pq,
exact pa,
end
Replace sorry with the correct Lean code.❌
✅
❌
❌