proposition: Lemma commandTwice : forall (c1 c2 : Comp bool), Pr [ b1 <-$ c1; b2 <-$ c2; ret (b1 && b2)] == (Pr [c1] * Pr[c2])%rat.
proof: Proof. intuition. simpl. repeat rewrite sumList_bool; intuition. simpl. destruct (EqDec_dec bool_EqDec false true); try discriminate. destruct (EqDec_dec bool_EqDec true true); try congruence. repeat rewrite ratMult_0_r. repeat rewrite <- ratAdd_0_r. repeat rewrite ratMult_0_r. repeat rewrite <- ratAdd_0_l. rewrite ratMult_1_r. intuition. eapply getSupport_NoDup. edestruct in_getSupport_or_evalDist_0. left. eauto. right. rewrite H. eapply ratMult_0_l. eapply getSupport_NoDup. edestruct in_getSupport_or_evalDist_0. left. eauto. right. rewrite H. eapply ratMult_0_l. eapply getSupport_NoDup. edestruct in_getSupport_or_evalDist_0. left. eauto. right. rewrite H. eapply ratMult_0_l. Qed.
imports: Crypto FCF RndNat