+
+(* The case of G2 is more complex. We should start introducing x and the inductive hypothesis
+ IH: ∃m. x = add m m ∨ x = S (add m m)
+At this point we should assume the existence of m enjoying the inductive hypothesis. To
+eliminate the existential from the context we can just use the case tactic. This situation where
+we introduce something into the context and immediately eliminate it by case analysis is
+so frequent that Matita provides a convenient shorthand: you can just type a single "*".
+The star symbol should be reminiscent of an explosion: the idea is that you have a structured
+hypothesis, and you ask to explode it into its constituents. In the case of the existential,
+it allows to pass from a goal of the shape
+ (∃x.P x) → Q
+to a goal of the shape
+ ∀x.P x → Q
+*)
+ |#x *
+(* At this point we are left with a new goal with the following shape
+ G3: ∀m. x = add m m ∨ x = S (add m m) → ....
+We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and then reason by
+cases on this hypothesis. It is the same situation as before: we explode the disjunctive
+hypothesis into its possible consituents. In the case of a disjunction, the * tactic allows
+to pass from a goal of the form
+ A∨B → Q
+to two subgoals of the form
+ A → Q and B → Q
+*)
+ #m * #eqx
+(* In the first subgoal, we are under the assumption that x = add m m. The half of (S x)
+is hence m, and we have to prove the right branch of the disjunction.
+In the second subgoal, we are under the assumption that x = S (add m m). The halh of (S x)
+is hence (S m), and have to follow the left branch of the disjunction.
+*)
+ [@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … m) /2/ | @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) normalize /2/