title: How does elim work in Coq on /\ and \/?
body: <p>In <a href="https://coq.inria.fr/tutorial/1-basic-predicate-calculus" rel="nofollow noreferrer">Coq Tutorial</a>, section 1.3.1 and 1.3.2, there are two <code>elim</code> applications:
  The first one:</p>
  
  <pre><code>1 subgoal
  
    A : Prop
    B : Prop
    C : Prop
    H : A /\ B
    ============================
     B /\ A
  </code></pre>
  
  <p>after applying <code>elim H</code>,</p>
  
  <pre><code>Coq &lt; elim H.
  1 subgoal
  
    A : Prop
    B : Prop
    C : Prop
    H : A /\ B
    ============================
     A -&gt; B -&gt; B /\ A
  </code></pre>
  
  <p>The second one:</p>
  
  <pre><code>1 subgoal
  
    H : A \/ B
    ============================
     B \/ A
  </code></pre>
  
  <p>After applying <code>elim H</code>,</p>
  
  <pre><code>Coq &lt; elim H.
  2 subgoals
  
    H : A \/ B
    ============================
     A -&gt; B \/ A
  
  subgoal 2 is:
   B -&gt; B \/ A
  </code></pre>
  
  <p>There are three questions. First, in the second example, I don't understand what inference rule (or, logical identity) is applied to the goal to generate the two subgoals. It is clear to me for the first example, though.</p>
  
  <p>The second question, according to the manual of Coq, <code>elim</code> is related to inductive types. Therefore, it appears that <code>elim</code> cannot be applied here at all, because I feel that there are no inductive types in the two examples (forgive me for not knowing the definition of inductive types). Why can <code>elim</code> be applied here?</p>
  
  <p>Third, what does <code>elim</code> do in general? The two examples here don't show a common pattern for <code>elim</code>. The official manual seems to be designed for very advanced users, since they define a term upon several other terms that are defined by even more terms, and their language is ambiguous.</p>
  
  <p>Thank you so much for answering!</p>