discussions a avoir d'urgence: acces a la memoire initiale dans les posts, ou extension de call pour faciliter l'instantiation des lemmes avec variables quantifiees?
idees: un mot cle de memoire old accessible uniquement en post x{old}, x{old.`1}, x{old.`2}

extention a fun:
  eqobs_in

extention:
  wp
  sp





rnd avec 6 arguments doit etre implemente en term de seq conseq et rnd...

rnd avec 1 argument : <= 
lemma foo : bd_hoare [M.f : true ==> res] <= (1%r/2%r).
fun.
seq 1 : true
        (1%r) (1%r/2%r) (0%r) _
       ( mu {0,1} (lambda (y0 : bool), x = y0) <= 1%r / 2%r &&
               forall (v : bool),
               in_supp v {0,1} => x = v => (lambda (y0 : bool), x = y0) v).
 admit.
trivial. 
rnd => //.
hoare;trivial.
trivial.




regle seq : 
  regle de base: seq i : R d1 d2 d3 d4

0: d1d2 + d3d4 ? d
1: {P} c1 {R}  ?d1
2: {R} c2 {Q}  ?d2
3: {P} c1 {!R} ?d3
4: {!R} c2 {Q} ?d4
---------------------------  
  {P} c1;c2 {Q} ? d   

regle avec inv : seq i R I d1 d2 d3 d4 

on commence pas faire un cut de hoare {P} c1 {I}
seq i : I (d1+d3) (d3+d4) 0 _
0 rien
1 bdhoare split R d1 d3
  suivit application hoare bdhoare => bdhoare and
2 case (pour bd_hoare) 
3 utilisation de hoare 
4 _ exists pas car d3 = 0