How does one prove (forall x, P x /\ Q x) -> (forall x, P x) in Coq? Been trying for hours and can't figure out how to break down the antecedent to something that Coq can digest. (I'm a newb, obviously 🙂
R – How to prove (forall x, P x /\ Q x) -> (forall x, P x)
coqproof
Best Answer
You can do it more quickly by just applying H, but this script should be more clear.