(*#* #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.