This issue is consisted of one problem and one bug.

**Problem: `cc` treats an `OfNat.ofNat` term as an atomic value in the default config**
In the default `CCConfig`, the `values` field is set to `true` so `cc` treats an `OfNat.ofNat` term as an atomic and it doesn't unify `OfNat` instances.
This problem can be solved simply by setting `values := false` by default.

**Bug: `cc` tries to disprove `@OfNat α (nat_lit n) i₁ ≠ @OfNat α (nat_lit n) i₂` where `α` is `ℕ` or `ℤ` and `i₁` & `i₂` is not alpha-equivalent but def_eq**
`cc` tactic has a mechanism to disprove equality between two different values of `ℕ`, `ℤ`, `Char` & `String`, in the function `propagateEqUp`. This mechanism is trigered when the root representations of two values are not alpha-equivalent, so this example fails.
```lean
local instance instOfNatNat' (n : ℕ) : OfNat ℕ n where
  ofNat := n

example : @OfNat.ofNat ℕ (nat_lit 0) (instOfNatNat _) =
    @OfNat.ofNat ℕ (nat_lit 0) (instOfNatNat' _) := by
  cc
/-
application type mismatch
  (bne_iff_ne 0 0).1 (Eq.refl true)
argument has type
  true = true
but function has type
  (0 != 0) = true → 0 ≠ 0
-/
```
So we strengthen the condition in `propagateEqUp`. For the detail, refer to docs in this function.

This issue is consisted of one problem and one bug.

**Problem: `cc` treats an `OfNat.ofNat` term as an atomic value in the default config**
In the default `CCConfig`, the `values` field is set to `true` so `cc` treats an `OfNat.ofNat` term as an atomic and it doesn't unify `OfNat` instances.
This problem can be solved simply by setting `values := false` by default.

**Bug: `cc` tries to disprove `@OfNat α (nat_lit n) i₁ ≠ @OfNat α (nat_lit n) i₂` where `α` is `ℕ` or `ℤ` and `i₁` & `i₂` is not alpha-equivalent but def_eq**
`cc` tactic has a mechanism to disprove equality between two different values of `ℕ`, `ℤ`, `Char` & `String`, in the function `propagateEqUp`. This mechanism is trigered when the root representations of two values are not alpha-equivalent, so this example fails.
```lean
local instance instOfNatNat' (n : ℕ) : OfNat ℕ n where
  ofNat := n

example : @OfNat.ofNat ℕ (nat_lit 0) (instOfNatNat _) =
    @OfNat.ofNat ℕ (nat_lit 0) (instOfNatNat' _) := by
  cc
/-
application type mismatch
  (bne_iff_ne 0 0).1 (Eq.refl true)
argument has type
  true = true
but function has type
  (0 != 0) = true → 0 ≠ 0
-/
```
So we strengthen the condition in `propagateEqUp`. For the detail, refer to docs in this function.

This issue is consisted of one problem and one bug.

**Problem: `cc` treats an `OfNat.ofNat` term as an atomic value in the default config**
In the default `CCConfig`, the `values` field is set to `true` so `cc` treats an `OfNat.ofNat` term as an atomic and it doesn't unify `OfNat` instances.
This problem can be solved simply by setting `values := false` by default.

**Bug: `cc` tries to disprove `@OfNat α (nat_lit n) i₁ ≠ @OfNat α (nat_lit n) i₂` where `α` is `ℕ` or `ℤ` and `i₁` & `i₂` is not alpha-equivalent but def_eq**
`cc` tactic has a mechanism to disprove equality between two different values of `ℕ`, `ℤ`, `Char` & `String`, in the function `propagateEqUp`. This mechanism is trigered when the root representations of two values are not alpha-equivalent, so this example fails.
```lean
local instance instOfNatNat' (n : ℕ) : OfNat ℕ n where
  ofNat := n

example : @OfNat.ofNat ℕ (nat_lit 0) (instOfNatNat _) =
    @OfNat.ofNat ℕ (nat_lit 0) (instOfNatNat' _) := by
  cc
/-
application type mismatch
  (bne_iff_ne 0 0).1 (Eq.refl true)
argument has type
  true = true
but function has type
  (0 != 0) = true → 0 ≠ 0
-/
```
So we strengthen the condition in `propagateEqUp`. For the detail, refer to docs in this function.