x,y:T. P(x) 
(x R y) P(y)T:Type, P:(T
Prop), R:(TTProp). R preserves P 
Prop| Who Cites preserved by? | |
| preserved_by | Def R preserves P == x,y:T. P(x) (x R y) P(y) |
| Thm* T:Type, P:(TProp), R:(TTProp). R preserves P Prop |
| Syntax: | R preserves P | has structure: | preserved_by(T; R; P) |
About:
 |  |  |  |  |  |  |  |