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 inductiondef 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

• Principle of explosion

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)