-The only way we have to prove an existential goal is by exhibiting the witness, that in the case
-of first goal is O. We do it by apply the term called ex_intro instantiated by the witness.
-Then, it is clear that we must follow the left branch of the disjunction. One way to do it is by
-applying the term or_introl, that is the first constructor of the disjunction. However,
-remembering the names of constructors can be annyoing: we can invoke the application of the n-th
-constructor of an inductive type (inferred by the current goal) by typing %n. At this point
-we are left with the subgoal O = add O O, that is closed by computation.
-It is worth to observe that invoking automation at depth /3/ would also automatically close G1.
+The only way we have to prove an existential goal is by exhibiting the witness,
+that in the case of first goal is O. We do it by apply the term called ex_intro
+instantiated by the witness. Then, it is clear that we must follow the left branch
+of the disjunction. One way to do it is by applying the term or_introl, that is
+the first constructor of the disjunction. However, remembering the names of
+constructors can be annyoing: we can invoke the application of the n-th
+constructor of an inductive type (inferred by the current goal) by typing %n. At
+this point we are left with the subgoal O = add O O, that is closed by
+computation. It is worth to observe that invoking automation at depth /3/ would
+also automatically close G1.