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

   1 (*#* #stop file *)
   2
   3 Require Export pr0_defs.
   4
   5       Inductive pr1 : T -> T -> Prop :=
   6          | pr1_r: (t:?) (pr1 t t)
   7          | pr1_u: (t2,t1:?) (pr0 t1 t2) -> (t3:?) (pr1 t2 t3) -> (pr1 t1 t3).
   8
   9       Hint pr1 : ltlc := Constructors pr1.
  10
  11    Section pr1_props. (******************************************************)
  12
  13       Theorem pr1_pr0: (t1,t2:?) (pr0 t1 t2) -> (pr1 t1 t2).
  14       XEAuto.
  15       Qed.
  16
  17       Theorem pr1_t: (t2,t1:?) (pr1 t1 t2) ->
  18                       (t3:?) (pr1 t2 t3) -> (pr1 t1 t3).
  19       Intros until 1; XElim H; XEAuto.
  20       Qed.
  21
  22       Theorem pr1_tail_1: (u1,u2:?) (pr1 u1 u2) ->
  23                           (t:?; k:?) (pr1 (TTail k u1 t) (TTail k u2 t)).
  24       Intros; XElim H; XEAuto.
  25       Qed.
  26
  27       Theorem pr1_tail_2: (t1,t2:?) (pr1 t1 t2) ->
  28                           (u:?; k:?) (pr1 (TTail k u t1) (TTail k u t2)).
  29       Intros; XElim H; XEAuto.
  30       Qed.
  31
  32    End pr1_props.
  33
  34       Hints Resolve pr1_pr0 pr1_t pr1_tail_1 pr1_tail_2 : ltlc.