1
(* correct failure of injection/discriminate on types whose inductive
2
status derives from the substitution of an argument *)
4
Inductive t : nat -> Type :=
5
| M : forall n: nat, nat -> t n.
7
Lemma eq_t : forall n n' m m',
8
existT (fun B : Type => B) (t n) (M n m) =
9
existT (fun B : Type => B) (t n') (M n' m') -> True.
17
Lemma eq_t' : forall n n' : nat,
18
existT (fun B : Type => B) (t n) (M n 0) =
19
existT (fun B : Type => B) (t n') (M n' 1) -> True.
22
discriminate H || exact I.