helm/coq-contribs/LAMBDA-TYPES/cpr0_defs.v

   1 (*#* #stop file *)
   2
   3 Require Export contexts_defs.
   4 Require Export pr0_defs.
   5
   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)).
  10
  11       Hint cpr0 : ltlc := Constructors cpr0.