proposition: Lemma find_first_indep : (forall x, P x <-> Q x) -> forall l, find_first P P_dec l = find_first Q Q_dec l.
proof: Proof. induction l; simpl. refl. destruct (P_dec a); destruct (Q_dec a); try rewrite H in *; try tauto. rewrite IHl. refl. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)