proposition: Lemma triple_while: forall P b c, {{atrue b //\\ P}} c {{P}} -> {{P}} WHILE b c {{afalse b //\\ P}}.
proof: Proof. unfold triple; intros P b c T s s' E. dependent induction E; intros. - split; auto. - eapply IHE2; eauto. apply T with s; auto. split; auto. Qed.
imports: Coq(ZArith Psatz Bool String List Wellfounded Program.Equality) Coq(FunctionalExtensionality) CDF(IMP Sequences)