morph Pendant2While: Pendant ==> While {
  Stm[ass](V,E)                              ==> << skip; >>
     [svp](V,E)       E()=>E                 ==> << <V> := <E>; >>
     [skip]()                                ==> << skip; >>
     [if](E,S)        E()=>E,S()=>S          ==> << if <E> then <S> >>
     [ifelse](E,S,S2) E()=>E,S()=>S,S2()=>S2 ==> << if <E> then <S> else <S2> >>
     [while](E,S)     E()=>E,S()=>S          ==> << while <E> do <S> >>

  Exp[neg](B)         B()=>B                 ==> << ! <B> >>
}