Merge PR #19063: Add tests for bug #4160.

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

test-suite/bugs/bug_4160_1.v

@@ -0,0 +1,23 @@
+(* -*- mode: coq; coq-prog-args: ("-indices-matter") -*- *)
+Axiom proof_admitted : False.
+Tactic Notation "admit" := case proof_admitted.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@ paths _ x y) : type_scope.
+Inductive String : Set :=
+| empty : String
+| string (c : bool) (cs : String) : String.
+Definition head_type (s : String) : Set :=
+  match s with
+  | empty => unit
+  | string _ _ => bool
+  end.
+Definition head (s : String) : head_type s :=
+  match s return head_type s with
+  | empty => tt
+  | string c _ => c
+  end.
+Definition ne_head (x y : bool) (xs ys: String)
+: string x xs = string y ys -> head (string x xs) = head (string y ys).
+Proof.
+  intro H.
+  Fail destruct H.
+Abort.

test-suite/bugs/bug_4160_2.v

@@ -0,0 +1,11 @@
+Inductive paths {A : Set} (a : A) : forall _ : A, Set := idpath : paths a a.
+Inductive bool := B.
+Inductive String : Set := string (c : bool) : String.
+Definition head_type (s : String) : Set :=
+match s with string _ => bool end.
+Axiom head : forall s : String, head_type s.
+Definition ne_head (x y : bool) (H : paths (string x) (string y)) :
+paths (head (string x)) (head (string y)).
+Proof.
+Fail case H.
+Abort.