Commit 97ff136d authored by charguer's avatar charguer


parent f7b19ca1
......@@ -275,6 +275,7 @@ Lemma Rule_mlist_length : forall A `{EA:Enc A} (L:list A) (p:loc),
POST (fun (r:int) => \[r = length L] \* p ~> MList L).
Proof using.
intros. gen p. induction_wf: list_sub_wf L; intros. xcf.
(* fold val_mlist_length *)
xapps~. xif ;=> C.
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p' L' EL.
xapps. xapps~ IH. xchange (MList_cons p).
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment