proposition: Lemma find_inject : forall (A B : Type) v (f : (nat * A) -> B) sigma, find X.eq_bool v (map (fun xt => (inject (fst xt), f xt)) sigma) = find Nat.eqb (inject_inv v) (map (fun xt => (fst xt, f xt)) sigma).
proof: Proof. fix find_inject 5. intros C B v f sigma; case sigma; clear sigma. apply eq_refl. intros p l; case p; clear p. intros n c; simpl. destruct (eq_nat_dec (inject_inv v) n) as [v_eq_n | v_diff_n]. subst n; rewrite Hinject1. generalize (X.eq_bool_ok v v); case (X.eq_bool v v); [intros _ | intro v_diff_v; apply False_rect; apply v_diff_v; apply eq_refl]. rewrite Nat.eqb_refl; apply eq_refl. generalize (X.eq_bool_ok v (inject n)); case (X.eq_bool v (inject n)); [intro v_eq_n | intros _]. subst v; apply False_rect; apply v_diff_n; rewrite Hinject2; apply eq_refl. generalize (decidable_set.beq_nat_ok (inject_inv v) n). case (Nat.eqb (inject_inv v) n); [intro v_eq_n | intros _]. apply False_rect; apply v_diff_n; assumption. apply find_inject. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)