Coq < Lemma ejemplo1:(m,m':memory)(b:bexpr)(c:com)  
(semcom m (while b c) m')->  
     (semcom m (cond b (seq  
                            c  
                            (while b c))  
                            skip)  
                     m').