tr:|E| List. P(tr) 
Q(tr)E:Structure, P,Q:((|E| List)
Prop). (P refines Q) 
PropS:Structure. |S| Type
Q)(L) == P(L) & Q(L)T:Type, P,Q:(TProp). (P Q) TProp
Top Type{i'}A:Type, B:(AType), p:(a:AB(a)). 1of(p) A Type| Who Cites tr refines? | |
| tr_refines |
Def P refines Q == tr:|E| List. P(tr) Q(tr) |
| Thm* E:Structure, P,Q:((|E| List)Prop). (P refines Q) Prop | |
| carrier | Def |S| == 1of(S) |
| Thm* S:Structure. |S| Type | |
| prop_and |
Def (P Q)(L) == P(L) & Q(L) |
| Thm* T:Type, P,Q:(TProp). (P Q) TProp | |
| struct |
Def Structure == TypeTop |
| Thm* struct{i:l} Type{i'} | |
| pi1 | Def 1of(t) == t.1 |
| Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A | |
| top | Def Top == Void given Void |
|
Thm* Top Type |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |