proposition: Lemma candidate_equiv l1 l2 : lequiv l1 l2 -> lequiv (candidate_list l1) (candidate_list l2).
proof: Proof. intros H1 a. repeat rewrite candidate_in. split; intros (i, (f, (Hf, (Hf1, Hf2)))); exists i; exists f; auto. - repeat split; auto; unfold lequiv in H1; rewrite <- H1; auto. - repeat split; auto; unfold lequiv in H1; rewrite H1; auto. Qed.
imports: ZArith List