At this point we want to prove A from A or ~A. And we go by cases on A. In the first line we say we want to use the elimination rule on "or", and then proceed by cases on the disjunction. The rest if the reply of Coq: We get two sub-goals. The first sub-goal is A, assuming A. The second sub-goal will still be A, to be proved by assuming not A. We tackle first the first sub-goal: We have to establish A, having A in the assumptions. So, this is trivial and this is what is said in the following slide: by using assumption, I immediately close the goal, and so I remain with just one sub-goal left, which is to prove A by assuming not A.

---