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

   1 Require pr1_confluence.
   2 Require pc1_defs.
   3
   4 (*#* #stop file *)
   5
   6    Section pc1_trans. (******************************************************)
   7
   8       Theorem pc1_t: (t2,t1:?) (pc1 t1 t2) ->
   9                      (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
  10       Intros; Repeat Pc1Unfold; Pr1Confluence; XEAuto.
  11       Qed.
  12
  13       Theorem pc1_pr0_u2: (t0,t1:?) (pr0 t0 t1) ->
  14                           (t2:?) (pc1 t0 t2) -> (pc1 t1 t2).
  15       Intros; Apply (pc1_t t0); XAuto.
  16       Qed.
  17
  18       Theorem pc1_tail: (u1,u2:?) (pc1 u1 u2) -> (t1,t2:?) (pc1 t1 t2) ->
  19                         (k:?) (pc1 (TTail k u1 t1) (TTail k u2 t2)).
  20       Intros; EApply pc1_t; [ EApply pc1_tail_1 | EApply pc1_tail_2 ]; XAuto.
  21       Qed.
  22
  23    End pc1_trans.
  24
  25       Hints Resolve pc1_t pc1_tail : ltlc.