EQUALITY

  rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

H >> ext == in A by intro equality A n
* >> A in
* >> A ext
*
* >> A ext

The default for n is 1.

. H >> (== in A) in by intro
* >> A in
* >> in A
*
* >> in A

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* canonical . H >> axiom in (a in A) by intro
* >> a in A

. H,x:T, >> x in T by intro

This rule doesn't work when T is a set or quotient term, since intro will invoke the equality rule for the set or quotient type, respectively. In any case, the equality rule can be used.