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

   1 (*#* #stop file *)
   2
   3 Require subst1_confluence.
   4 Require csubst1_defs.
   5 Require pr3_gen_context.
   6 Require pc3_defs.
   7 Require pc3_props.
   8
   9    Section pc3_gen_context. (************************************************)
  10
  11       Theorem pc3_gen_cabbr: (c:?; t1,t2:?) (pc3 c t1 t2) -> (e:?; u:?; d:?)
  12                              (drop d (0) c (CTail e (Bind Abbr) u)) ->
  13                              (a0:?) (csubst1 d u c a0) ->
  14                              (a:?) (drop (1) d a0 a) ->
  15                              (x1:?) (subst1 d u t1 (lift (1) d x1)) ->
  16                              (x2:?) (subst1 d u t2 (lift (1) d x2)) ->
  17                              (pc3 a x1 x2).
  18       Intros; Pc3Unfold; Repeat Pr3GenContext.
  19       Subst1Confluence; Rewrite H3 in H5; Clear H3 x3; XEAuto.
  20       Qed.
  21
  22    End pc3_gen_context.