        (assume [f absurd]
          (qed (f A))))
 
-(defterm neg
+(defterm not
   "Logical negation."
   [[A :type]]
   (==> A absurd))
 
 (example
- (type-of neg) => '(Π [A ✳] ✳))
+ (type-of not) => '(Π [A ✳] ✳))
 
 (defthm absurd-intro
   "Introduction rule for absurdity."
   [[A :type]]
-  (==> A (neg A)
+  (==> A (not A)
        absurd))
 
 ;; (proof absurd-intro

;;              (lambda [z (==> A B C)]
;;                z x y)))))

(proof land-intro
       :script
       (assume [x A
                y B

(ns latte.prop
  (:refer-clojure :exclude [and or not])
  (:require [clj-by.example :refer [example do-for-example]])
  (:require [latte.core :as latte :refer [defterm term type-of defthm
                                          lambda forall assume proof]])
