eq:EqDecider(A), P:(A
TypeProp), x:A, v:Type.
Thm*
y
dom(x : v). w=x : v(y) 
P(y,w) 
P(x,v)d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true
| Theorem | Name |
| eq:EqDecider(A), P:(ATypeProp), x:A, v:Type.
Thm* ydom(x : v). w=x : v(y) P(y,w) P(x,v) | [fpf-all-single-decl] |
| cites the following: | |
| d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true | [eqof_eq_btrue] |