+qed.
+
+inductive bar_list (A:Set): Set \def
+ | bar_nil: bar_list A
+ | bar_cons: A \to bar_list A \to bar_list A.
+
+alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
+theorem stupid2:
+ \forall A:Set.\forall x:A.\forall l:bar_list A.
+ bar_nil A = bar_cons A x l \to False.
+ intros.
+ discriminate H.
+qed.