proposition: Lemma removeFirst_length : forall (A : Set)(eqd : eq_dec A)(ls : list A) a, In a ls -> S (length (removeFirst eqd ls a)) = length ls.
proof: Proof. induction ls; intuition; simpl in *. intuition. subst. f_equal. destruct (eqd a0 a0). trivial. congruence. destruct (eqd a0 a); subst. trivial. simpl. f_equal. eauto. Qed.
imports: Crypto Permutation CompFold Array FCF State