proposition: Lemma eq_find_eq : equivalence _ eqA -> forall B a a' l, eq_bool a a' = true -> find (B := B) a l = find a' l.
proof: Proof. intro eq_proof. fix eq_find_eq 4. intros B a a' l; case l; clear l; simpl. intros _; reflexivity. intros p l; case p; clear p; simpl. intros a'' b a_eq_a'; case_eq (eq_bool a a''); case_eq (eq_bool a' a''). intros _ _; reflexivity. intros a'_diff_a'' a_eq_a''; absurd (eqA a' a''). generalize (eq_bool_ok a' a''); rewrite a'_diff_a''; intro H; exact H. case eq_proof; intros Req Teq Seq. apply (Teq a' a a''). apply Seq; generalize (eq_bool_ok a a'); rewrite a_eq_a'; intro H; exact H. generalize (eq_bool_ok a a''); rewrite a_eq_a''; intro H; exact H. intros a'_eq_a'' a_diff_a''; absurd (eqA a a''). generalize (eq_bool_ok a a''); rewrite a_diff_a''; intro H; exact H. case eq_proof; intros Req Teq Seq. apply (Teq a a' a''). generalize (eq_bool_ok a a'); rewrite a_eq_a'; intro H; exact H. generalize (eq_bool_ok a' a''); rewrite a'_eq_a''; intro H; exact H. intros _ _; apply eq_find_eq; assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)