Coqで排中律の二重否定を証明（を一般化）

この前の排中律の二重否定の証明
https://zenn.dev/sabataro/articles/eeb421b7f0645247a1ae
を少し一般化してみました。
Coqでの否定の定義は以下のようになっています。

Definition not a:=a->False.

Falseの部分を全て一般のb：Propに変えても全く同じように証明できます。

Goal forall a b:Prop,
(a\/(a->b)->b)->b.
Proof.
intros.
apply H.
right.
intro.
apply H.
left.
assumption.
Qed.

つまり、この証明ではFalse固有の性質（Falseが仮定にあれば何でも証明できる）を使っておらず、最小論理の範疇で証明できるということですね。
以下はCoqの動作を表した図です。

  ────────────────────────────────────────────── assumption      
  a:Prop , b:Prop , H:a ∨ (a → b) → b , H0:a ⊢ a                 
──────────────────────────────────────────────────────── left    
a:Prop , b:Prop , H:a ∨ (a → b) → b , H0:a ⊢ a ∨ (a → b)         
──────────────────────────────────────────────────────── apply[H]
     a:Prop , b:Prop , H:a ∨ (a → b) → b , H0:a ⊢ b              
──────────────────────────────────────────────────────── intro   
       a:Prop , b:Prop , H:a ∨ (a → b) → b ⊢ a → b               
──────────────────────────────────────────────────────── right   
    a:Prop , b:Prop , H:a ∨ (a → b) → b ⊢ a ∨ (a → b)            
──────────────────────────────────────────────────────── apply[H]
         a:Prop , b:Prop , H:a ∨ (a → b) → b ⊢ b                 
──────────────────────────────────────────────────────── intros  
        ⊢ ∀a:Prop, ∀b:Prop, (a ∨ (a → b) → b) → b