a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)
TProp).
Thm* (with ds: ds action a:T precondition a(v) is P s v)
MsgAx:T. (x nil) 
Falsel:T List, a,x:T. (x [a / l]) x = a 
(x l)| Rank | Theorem | Name |
| 2 | a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp).
Thm* (with ds: ds action a:T precondition a(v) is P s v) MsgA | [ma-single-pre_wf] |
| cites the following: | ||
| 0 | x:T. (x nil) False | [nil_member] |
| 1 | l:T List, a,x:T. (x [a / l]) x = a (x l) | [cons_member] |