proposition: Lemma triple_skip: [[ emp ]] SKIP [[ emp ]].
proof: Proof. intros R IND s h PRE. exists s, h; split; auto. apply star_refl. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality PropExtensionality) CDF(IMP Sequences)