M:sm{i:l}(), I:(M.state
(M.action List)Prop).
(x:M.state. M.init(x) 
I(x,nil))
(s0,x:M.state, act:M.action, x':M.state, l:M.action List.
M.init(s0) trace_reachable(M;s0;l;x) I(x,l) M.trans(x,act,x') I(x',l @ [act]))
(M |= always s,t.I(s,t))Q:((T List)Prop).
Q(nil) (ys:T List, x:T. Q(ys) Q(ys @ [x])) (zs:T List. Q(zs))