proposition: Remark cexecinf_while_true_skip: forall s, cexecinf s (WHILE TRUE SKIP).
proof: Proof. cofix CIH; intros. eapply cexecinf_while_2. auto. apply cexec_skip. apply CIH. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)