proposition: Lemma checkBad_app_cons : forall ls d r, checkBad (ls ++ (d, r) :: nil) = checkBad ((d , r) :: ls).
proof: Proof. intuition. symmetry. eapply checkBad_permutation. eapply Permutation_cons_append. Qed.
imports: Crypto Permutation Broken.ConstructedFunc State FCF