I am trying to prove a theorem in Coq and I am not able to solve an issue that occurs. I am trying to solve:
forall A B C: Prop, A\/(B\/C)->(A\/B)\/C.
Proof.
intros.
destruct H as [H1 | [H2 | H3 ]].
Case H1.
and in this last line I get the following error "Error: The reference Case was not found in the current environment."
I am new to Coq so I do not know what that really means. I did some research on the Internet but I did not manage to find a solution. Does anyone have an idea of what this problem comes from?
You've destructed the hypothesis, so you're already analyzing each case.
Use left and right to manipulate the disjunction in the conclusion, and assumption when a hypothesis and the conclusion are the same.