Scheme Equality for nat + Require Import Coq.Logic.Eqdep_dec. breaks inversion ("Illegal application" at Qed)

[JasonGross]

(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+undeclared-scope,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+deprecated-typeclasses-transparency-without-locality,-ltac2-missing-notation-var,unsupported-attributes" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-R" "theories" "NeuralNetInterp" "-top" "NeuralNetInterp.Torch.Slicing.Instances") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 191 lines to 94 lines, then from 104 lines to 20 lines, then from 33 lines to 538 lines, then from 539 lines to 20 lines, then from 33 lines to 533 lines, then from 538 lines to 69 lines, then from 59 lines to 19 lines, then from 24 lines to 20 lines *)
(* coqc version 8.19+alpha compiled with OCaml 4.14.1
   coqtop version JasonGross-X1:/home/jgross/Downloads/coq/coq-master/_build/default,master (61ee398ed32f9334dd664ea8ed2697178e6e3844)
   Expected coqc runtime on this file: 0.307 sec *)
Require Import Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions.
Axiom proof_admitted : False.
Inductive t : nat   -> nat   -> Type :=
| elipsis {r} : t r r.
Inductive t_relation : forall {ri ro}, relation (@t ri ro) :=
| R_elipsis {r} : t_relation (elipsis (r:=r)) (elipsis (r:=r))
.
#[export] Instance t_relation_Transitive0 {ri ro} : Transitive (@t_relation ri ro).
Proof.
  intros x y z H1 H2.
  induction H1.
  inversion H2.
  (* 1 goal (ID 70)

  r : nat
  z : t r r
  H2 : t_relation elipsis z
  r0 : nat
  H : r0 = r
  H0 : r = r
  H1 : existT (fun x : nat => {x0 : nat & t x x0}) r
         (existT (fun x : nat => t r x) r elipsis) =
       existT (fun x : nat => {x0 : nat & t x x0}) r (existT (fun x : nat => t r x) r z)
  ============================
  t_relation elipsis z
*)
  all: abstract case proof_admitted.
Qed.

(*
Require Import Coq.Logic.Eqdep_dec.

#[export] Instance t_relation_Transitive0a {ri ro} : Transitive (@t_relation ri ro).
Proof.
  intros x y z H1 H2.
  induction H1.
  inversion H2.
  (* 1 goal (ID 76)

  r : nat
  z : t r r
  H2 : t_relation elipsis z
  r0 : nat
  H : r0 = r
  H0 : r = r
  H1 : existT (fun x : nat => {x0 : nat & t x x0}) r
         (existT (fun x : nat => t r x) r elipsis) =
       existT (fun x : nat => {x0 : nat & t x x0}) r (existT (fun x : nat => t r x) r z)
  ============================
  t_relation elipsis z
*)
  all: abstract case proof_admitted.
Qed.
*)
Scheme Equality for nat.

#[export] Instance t_relation_Transitive1 {ri ro} : Transitive (@t_relation ri ro).
Proof.
  intros x y z H1 H2.
  induction H1.
  inversion H2.
  all: abstract case proof_admitted.
Qed.
(* Warning: The equality scheme for nat
could not be used as Coq.Logic.Eqdep_dec has not been required.
[injection-missing-eqdep-dec,tactics,default]
*)

Require Import Coq.Logic.Eqdep_dec.

#[export] Instance t_relation_Transitive2 {ri ro} : Transitive (@t_relation ri ro).
Proof.
  intros x y z H1 H2.
  induction H1.
  inversion H2.
  (* 1 goal (ID 231)

  r : nat
  z : t r r
  H2 : t_relation elipsis z
  r0 : nat
  H : r0 = r
  H0 : r = r
  H1 : existT (fun x : nat => t r x) r elipsis = existT (fun x : nat => t r x) r z
  ============================
  t_relation elipsis elipsis
*)
  all: abstract case proof_admitted.
Qed.
(* Error: Illegal application:
The term "@t_relation" of type "forall ri ro : nat, relation (t ri ro)"
cannot be applied to the terms
 "projT1 s" : "nat"
 "projT1 s" : "nat"
 "elipsis" : "t (projT1 s) (projT1 s)"
 "projT2 s" : "t r (projT1 s)"
The 4th term has type "t r (projT1 s)" which should be a subtype of
 "t (projT1 s) (projT1 s)".
*)