proposition: Theorem compLoop_S : forall (A : Set)(eqda : EqDec A)(c : A -> Comp A) n a x, evalDist (compLoop _ c (S n) a) x == evalDist (a0 <-$ c a; compLoop eqda c n a0) x.
proof: Proof. induction n; intuition. unfold compLoop, allNatsLt. rewrite app_nil_l. unfold compFold. intuition. unfold compLoop, allNatsLt. fold allNatsLt. eapply eqRat_trans. rewrite compFold_app. eapply evalDist_seq_eq. intros. eapply IHn. intros. eapply eqRat_refl. dist_inline_first. comp_skip. unfold compLoop. eapply eqRat_trans. symmetry. eapply compFold_app. eapply comp_spec_eq_impl_eq. eapply (@compFold_eq _ _ (fun x y => True)). eapply list_pred_I. repeat rewrite app_length. simpl; intuition. intuition. Qed.
imports: FCF CompFold