proposition: Lemma Triple_skip: forall P, [[P]] SKIP [[P]].
proof: Proof. intros P s PRE. exists s; split; auto. apply cexec_skip. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)