+(*#* #stop file *)
+
+Require Export contexts_defs.
+Require Export pr0_defs.
+
+ Inductive cpr0 : C -> C -> Prop :=
+ | cpr0_refl : (c:?) (cpr0 c c)
+ | cpr0_cont : (c1,c2:?) (cpr0 c1 c2) -> (u1,u2:?) (pr0 u1 u2) ->
+ (k:?) (cpr0 (CTail c1 k u1) (CTail c2 k u2)).
+
+ Hint cpr0 : ltlc := Constructors cpr0.