3 Require Export contexts_defs.
4 Require Export pr0_defs.
6 Inductive cpr0 : C -> C -> Prop :=
7 | cpr0_refl : (c:?) (cpr0 c c)
8 | cpr0_cont : (c1,c2:?) (cpr0 c1 c2) -> (u1,u2:?) (pr0 u1 u2) ->
9 (k:?) (cpr0 (CTail c1 k u1) (CTail c2 k u2)).
11 Hint cpr0 : ltlc := Constructors cpr0.