proposition: Theorem vcgen_correct: forall P c Q, vcgen P c Q -> {{P}} erase c {{Q}}.
proof: Proof. unfold vcgen; intros. destruct H as (V1 & V2). eapply triple_consequence. eapply vcg_sound; eauto. auto. red; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)