gistfile1.txt

Unnamed_thm = 
fun (T' S' : Prop) (H : T' -> S') (H0 : (T' -> False) \/ S' -> False) =>
(fun H1 : (T' -> False) -> False =>
 (fun H2 : S' -> False =>
  (fun H3 : False => (fun H4 : False => False_ind False H4) H3)
    ((fun H3 : T' -> False => H1 H3)
       ((fun (H3 : False -> False) (H4 : T') =>
         (fun H5 : S' =>
          (fun H6 : False => (fun H7 : False => False_ind False H7) (H3 H6))
            (H2 H5)) (H H4)) (fun y : False => H1 (fun _ : T' => y)))))
   (fun H2 : S' => H0 (or_intror H2)))
  (fun H1 : T' -> False => H0 (or_introl H1))
     : forall T' S' : Prop,
       (T' -> S') -> ((T' -> False) \/ S' -> False) -> False

Argument scopes are [type_scope type_scope _ _]

hoge.v

Goal forall T' S' : Prop , (T' -> S') -> ((or (T' -> False) S') -> False) -> False.
Proof.
tauto.
Defined.

Print Unnamed_thm.