Leanマニュアルでは "object" も使っているが、混乱のもとなので「要素〈element〉」を使う。「インスタンス」も混乱のもとなので使わない。「型の要素」を使う。
型の要素が命題の証拠〈witness〉に対応する。次はセクションの定義：
variable (F : Type → Type) variable (s : ∀(X : Type), F X) #check s Nat
セクション s は、パイ型のセクション。このパイ型は型族（型引数を持つ型）の総称型／多相型と言っていい。セクションは総称型〈多相型〉の一般化要素になる。
- (要素 ： 型 ) の一般化が (一般化要素 : パイ型)
要素はポインターで、一般化要素はセクション。
命題の型宇宙では：
- (証拠 ： 命題) の一般化が (一般化証拠 : 全称命題)
命題〈型〉と証拠〈ポインター〉、あるいは証明〈関数〉を区別する。命題には命題演算〈コネクティブ〉があり、証明〈定理〉には証明のコネクティブがある。
証明〈計算〉から証明〈計算〉を作る手続き〈メタ計算〉を重視する構成的論理で考える。証明〈計算〉に関するメタ計算がリーズニング。
