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

* >>

* >>

*

* >>

The default fornis 1.

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

* >> A in

* >> in A

*

* >> in A

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

* >>

.`
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, theequality rule can be used.

`
`

Thu Sep 14 08:45:18 EDT 1995