Suppose we take a type
```
inductive Eg
| A | B
```

- how do we show that
`Eg.A <> Eg.B`

from first principles? (using only recursors?) - This is the same as showing
`Eg.A = Eg.B -> False`

.

- First, some gadgets: congruence of function arguments:

```
-- path induction
def fun_functional (f : A → B) (x y : A) (EQ : x = y) : f x = f y :=
Eq.recOn EQ (motive := fun k K_EQ_X => f x = f k) rfl
```

```
def false_elim (f : False) : α := False.rec f (motive := fun _ => α)
```

- Key idea: create a type by using the recursors of
`x, y`

such that when `x = y`

we have True and when `x <> y`

we have False. - Then, when given a proof that
`Eg.A = Eg.B`

, we can go through the cases and we want to produce false, we can use `Eq.rec`

on this type, and produce the inhabitant `True.intro`

for the cases when they are equal. Then, path induction / the recursor for equality will give us an inhabitant of `False`

, by promoting this to hold "in general".

```
abbrev Eg.noConfusionType' (x y : Eg) : Prop :=
x.casesOn (motive := fun _ => Prop)
(y.casesOn (motive := fun _ => Prop) True False)
(y.casesOn (motive := fun _ => Prop) False True)
```

- We show that this type is inhabited when
`x = x`

.

```
abbrev Eg.noConfusionType'_inhabitant_rfl : Eg.noConfusionType' x x :=
x.casesOn True.intro True.intro
```

- We show that if
`x <> y`

, then an inhabitant of `Eg.noConfusionType' x y`

produces `False`

.

```
abbrev Eg.def2 (x y : Eg) (NEQ: x ≠ y) (NC: Eg.noConfusionType' x y) : False :=
match H : x with
| .A =>
match K : y with
| .A => NEQ rfl
| .B => NC
| .B => match K : y with
| .A => NC
| .B => NEQ rfl
```

- How to translate the above into a raw formula?

```
Eg.rec (motive := fun x_1 =>
∀ (NEQ : x_1 ≠ y) (NC : Eg.noConfusionType' x_1 y), x = x_1 → (fun x NEQ NC => False) x_1 NEQ NC)
(fun NEQ NC H =>
Eg.rec (motive := fun x =>
∀ (NEQ : Eg.A ≠ x) (NC : Eg.noConfusionType' Eg.A x), y = x → (fun y NEQ NC => False) x NEQ NC)
(fun NEQ NC K => NEQ (Eq.refl Eg.A)) (fun NEQ NC K => NC) y NEQ NC (Eq.refl y))
(fun NEQ NC H =>
Eg.rec (motive := fun x =>
∀ (NEQ : Eg.B ≠ x) (NC : Eg.noConfusionType' Eg.B x), y = x → (fun y NEQ NC => False) x NEQ NC)
(fun NEQ NC K => NC) (fun NEQ NC K => NEQ (Eq.refl Eg.B)) y NEQ NC (Eq.refl y))
x NEQ NC (Eq.refl x)
```