Coqで排中律の二重否定を証明

Coqの論理は直観主義論理なので排中律が証明できない
代わりに排中律の二重否定を証明する

Goal forall a,~~(a\/~a).
Proof.
intro.
intro.
apply H.
right.
intro.
apply H.
left.
assumption.
Qed.

以下はこの証明スクリプトを実行したときのCoqの動作を表した図です
ProofWebというサイトを利用しました

─────────────────────────────── assumption   
a:Prop , H:¬(a ∨ ¬a) , H0:a ⊢ a              
──────────────────────────────────── left    
a:Prop , H:¬(a ∨ ¬a) , H0:a ⊢ a ∨ ¬a         
──────────────────────────────────── apply[H]
  a:Prop , H:¬(a ∨ ¬a) , H0:a ⊢ ⊥          
──────────────────────────────────── intro   
      a:Prop , H:¬(a ∨ ¬a) ⊢ ¬a              
──────────────────────────────────── right   
    a:Prop , H:¬(a ∨ ¬a) ⊢ a ∨ ¬a            
──────────────────────────────────── apply[H]
     a:Prop , H:¬(a ∨ ¬a) ⊢ ⊥              
──────────────────────────────────── intro   
         a:Prop ⊢ ¬¬(a ∨ ¬a)                 
──────────────────────────────────── intro   
        ⊢ ∀a:Prop, ¬¬(a ∨ ¬a)