aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_057.v
blob: e72ce0c5ec7746d7f422730cbee1df08c317008e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
Require Export Coq.Lists.List.

Polymorphic Fixpoint LIn (A : Type) (a:A) (l:list A) : Type :=
  match l with
    | nil => False
    | b :: m => (b = a) + LIn A a m
  end.

Polymorphic Inductive NTerm : Type :=
| cterm : NTerm
| oterm : list NTerm -> NTerm.

Polymorphic Fixpoint dummy {A B} (x : list (A * B)) : list (A * B) :=
  match x with
    | nil => nil
    | (_, _) :: _ => nil
  end.

Lemma foo :
  forall v t sub vars,
    LIn (nat * NTerm) (v, t) (dummy sub)
    ->
    (
      LIn (nat * NTerm) (v, t) sub
      *
      notT (LIn nat v vars)
    ).
Proof.
  induction sub; simpl; intros.
  destruct H.
  Set Printing Universes.
  try (apply IHsub in X). (* Toplevel input, characters 5-21:
Error: Universe inconsistency (cannot enforce Top.47 = Set). *)