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

   1 Require subst0_lift.
   2 Require drop_props.
   3 Require pr0_lift.
   4 Require pr2_defs.
   5
   6 (*#* #caption "main properties of predicate \\texttt{pr2}" *)
   7 (*#* #clauses pr2_props *)
   8
   9    Section pr2_lift. (*******************************************************)
  10
  11 (*#* #caption "conguence with lift" *)
  12 (*#* #cap #cap c, t1, t2 #alpha e in D, d in i *)
  13
  14       Theorem pr2_lift : (c,e:?; h,d:?) (drop h d c e) ->
  15                          (t1,t2:?) (pr2 e t1 t2) ->
  16                          (pr2 c (lift h d t1) (lift h d t2)).
  17
  18 (*#* #stop file *)
  19
  20       Intros until 2; XElim H0; Intros.
  21 (* case 1 : pr2_pr0 *)
  22       XAuto.
  23 (* case 2 : pr2_delta *)
  24       Apply (lt_le_e i d); Intros; DropDis.
  25 (* case 2.1 : i < d *)
  26       Rewrite minus_x_Sy in H0; [ Idtac | XAuto ].
  27       DropGenBase; Rewrite H0 in H; Simpl in H; XEAuto.
  28 (* case 2.2 : i >= d *)
  29       XEAuto.
  30       Qed.
  31
  32    End pr2_lift.
  33
  34       Hints Resolve pr2_lift : ltlc.