thf(const_true, type, (true : $i)).
thf(const_implies, type, (implies : $i > ($i > $i))).
thf(const_forall, type, (forall : ($i > $i) > $i)).
thf(const_eq, type, (eq: $i > ($i > $i))).
thf(const_false, type, (false : $i)).
thf(const_not, type, (not : ($i > $i))).

thf(modusPonens, axiom, (! [U : $i]: (((implies @ true @ U) = true) => (U = true)))).

thf(allIntro, axiom, (! [F : ($i > $i)]: (
  (! [X : $i]: ((F @ X) = true)) => ((forall @ F) = true)))).

thf(ax2, axiom, (! [A : $i, B : $i]: ((implies @ A @ (implies @ B @ A)) = true))).

thf(ax3, axiom, (! [A : $i, B : $i, C : $i]: (
  (implies  
    @ (implies @ A @ (implies @ B @ C)) 
    @ (implies @ (implies @ A @ B) @ (implies @ A @ C)))
  = true))).

thf(ax4, axiom, (! [X : $i, A : ($i > $i)]: (
  (implies 
    @ (forall @ A) 
    @ (A @ X)) = true))).

thf(ax5, axiom, (! [A : $i, B : ($i > $i)]: (
  (implies 
    @ (forall @ (^[X : $i]: (implies @ A @ (B @ X))))
    @ (implies @ A @ (forall @ B))) = true))).

thf(ax6, axiom, (! [X : $i]: ((eq @ X @ X) = true))).

thf(ax7, axiom, (! [X : $i, Y : $i, A : ($i > $i)]: (
  (implies 
    @ (eq @ X @ Y)
    @ (implies @ (A @ X) @ (A @ Y))) = true))).

thf(ax8, axiom, (! [A : $i]: ((implies @ A @ (eq @ A @ true)) = true))).

thf(ax9, axiom, ((eq @ false @ (forall @ (^[X : $i]: X))) = true)).

thf(ax10, axiom, (![A : $i]: (
  (eq 
    @ (not @ A)
    @ (implies @ A @ false)) = true))).

thf(explosion, conjecture, (! [A : $i, B : $i]: (
 (implies 
   @ A
   @ (implies @ (not @ A) @ B)) = true))).