quotients as indices of inductives seems sound

gistfile1.txt

  Axiom natMod7: Type.
  Axiom inj : nat -> natMod7.

Inductive Vector : natMod7 → Prop :=
| ttrue  : Vector (inj 0)
| ffalse : False -> Vector (inj 7).

Lemma eqq:  inj 7 = inj 0. Proof. Admitted.

Lemma ff: False.
Proof using.
  pose proof ttrue as H.
  rewrite <- eqq in H.
  inversion H.
  -
    (* cannot prove false: for inversion to pick only 1 case, it uses pattern matching, but pattern matching cannot distinguish between equiv elems of a quotient type even if they are syntactically different *)
 thread_info : biIndex
  _Σ : gFunctors
  Σ : cpp_logic thread_info _Σ
  gg : genv
  modd : module ⊧ gg
  H : Vector (inj 7)
  H1 : inj 0 = inj 7
  ============================
  False
*)
  -