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

   1 (*#* #stop file *)
   2
   3 Require subst1_defs.
   4 Require pr2_subst1.
   5 Require pr3_defs.
   6
   7    Section pr3_subst1_props. (***********************************************)
   8
   9       Theorem pr3_subst1: (c,e:?; v:?; i:?) (drop i (0) c (CTail e (Bind Abbr) v)) ->
  10                           (t1,t2:?) (pr3 c t1 t2) ->
  11                           (w1:?) (subst1 i v t1 w1) ->
  12                           (EX w2 | (pr3 c w1 w2) & (subst1 i v t2 w2)).
  13      Intros until 2; XElim H0; Clear t1 t2; Intros.
  14 (* case 1: pr3_refl *)
  15      XEAuto.
  16 (* case 2: pr3_single *)
  17      Pr2Subst1.
  18      LApply (H2 x); [ Clear H2; Intros H2 | XAuto ].
  19      XElim H2; XEAuto.
  20      Qed.
  21
  22    End pr3_subst1_props.
  23
  24       Tactic Definition Pr3Subst1 :=
  25          Match Context With
  26             | [ H0: (drop ?1 (0) ?2 (CTail ?3 (Bind Abbr) ?4));
  27                 H1: (pr3 ?2 ?5 ?6); H3: (subst1 ?1 ?4 ?5 ?7) |- ? ] ->
  28                LApply (pr3_subst1 ?2 ?3 ?4 ?1); [ Intros H_x | XAuto ];
  29                LApply (H_x ?5 ?6); [ Clear H_x H1; Intros H1 | XAuto ];
  30                LApply (H1 ?7); [ Clear H1; Intros H1 | XAuto ];
  31                XElim H1; Intros
  32             | _ -> Pr2Subst1.