P:(L:(T List)
(||L||-1)Prop).
Thm* Trans(T List)(_1 guarded_permutation(T;P) _2)
R:(TTProp), x,y,z:T. (x (R^*) y) 
(y (R^*) z) (x (R^*) z)| Rank | Theorem | Name |
| 2 | P:(L:(T List)(||L||-1)Prop).
Thm* Trans(T List)(_1 guarded_permutation(T;P) _2) | [guarded_permutation_transitivity] |
| cites the following: | ||
| 1 | R:(TTProp), x,y,z:T. (x (R^*) y) (y (R^*) z) (x (R^*) z) | [rel_star_transitivity] |