a':T. Q(a') 
a' = a)T:Type, a:T, Q:(T
Prop). (a = !x:T. Q(x)) 
Prop| Who Cites uni sat? | |
| uni_sat | Def a = !x:T. Q(x) == Q(a) & (a':T. Q(a') a' = a) |
| Thm* T:Type, a:T, Q:(TProp). (a = !x:T. Q(x)) Prop |
| Syntax: | a = !x:T. Q(x) | has structure: | uni_sat(T; a; x.Q(x)) |
About:
 |  |  |  |  |  |  |  |  |