+let corec div (n:nat) : stream ≝ scons n (div (S n)).
+
+axiom plus: nat → nat → nat.
+
+definition rtest2 : nat → stream → nat ≝
+ λm,s. match s with [ scons n l ⇒ plus m n ].
+
+(*
+let rec mkterm (n:nat) : nat ≝
+ match n with
+ [ O ⇒ O
+ | S m ⇒ mkterm m ]
+and mktyp (n:nat) : Type[0] ≝
+ match n with
+ [ O ⇒ nat
+ | S m ⇒ mktyp m ].*)
+
+inductive meee: Type[0] → Type[0] ≝ .
+
+inductive T1 : (Type[0] → Type[0]) → ∀B:Type[0]. nat → Type[0] → Type[0] ≝ .
+
+inductive T2 : (Type[0] → Type[0]) → ∀B:Type[0]. B → Type[0] → Type[0] ≝ .
+
+(* no content *)
+inductive T3 : (Type[0] → Type[0]) → CProp[2] ≝ .
+
+definition erase ≝ λX:Type[0].Type[0].
+
+axiom lt: nat → nat → Prop.
+
+inductive myvect (A: Type[0]) (b:nat) : nat → Type[0] ≝
+ myemptyv : myvect A b O
+ | mycons: ∀n. lt n b → A → myvect A b n → myvect A b (S n).
+
+inductive False: Prop ≝ .
+
+inductive Empty: Type[0] ≝ .
+
+inductive bool: Type[0] ≝ true: bool | false:bool.
+
+inductive eq (A:Type[1]) (a:A) : A → Prop ≝ refl: eq A a a.
+
+(* requires coercion *)
+definition cast_bug1 ≝
+ λH:eq Type[0] bool nat. S (match H return λA:Type[0].λ_.A with [ refl ⇒ true ]).
+
+(*
+(*BUG: Here we use eq_rect_Type0 in its poly-kinded form, but we only extracted
+ the one-kinded form. Require coercions *)
+definition cast_bug1' ≝
+ λH:eq Type[0] bool nat. S (eq_rect_Type0 Type[0] bool (λA:Type[0].λ_.A) true nat H).
+*)
+
+(* requires coercion in all branches *)
+definition cast_bug2 ≝
+ match true return λb.match b with [ true ⇒ nat → nat | false ⇒ bool ] with
+ [ true ⇒ S | false ⇒ false ]
+ O.
+
+(*BUG: try singleton elimination with constructor arguments to show bug in
+ DeBrujin indexes *)
\ No newline at end of file