helm/software/components/ng_tactics/README

   1 +letin: basta la refine fatta con occurcheck
   2 +cut:   letin; clearbody ~-1 (cosa sia ~-1 è da capirsi)
   3
   4 -generalize:
   5   a) verificare che tutti i termini selezionati siano convertibili
   6   b) spostare i termini selezionati nel contesto corrente/spostare il
   7      termine bucato sotto un lambda
   8   c) bucare e liftare deve essere fatto contemporaneamente
   9   d) poi usare tatticali per fare cut + apply
  10
  11 =fail:
  12 =id:
  13
  14 apply:
  15 applyS:
  16 intros:
  17 elim:
  18 cases:
  19 rewrite:
  20 ??replace: rewrite (?:A=B); [2: apply eq_a_b ]
  21 =auto/demodulate/solve_rewrite:
  22 change:
  23 clear/clearbody:
  24 destruct:
  25 inversion:
  26 lapply:
  27 ??compose:
  28 whd/simpl/normalize:
  29 fold:
  30 unfold:
  31
  32 assumption:
  33 constructor:
  34 exists:
  35 left:
  36 right:
  37 reflexivity:
  38 symmetry:
  39 transitivity:
  40 split:
  41
  42 decompose:
  43
  44 #####
  45 absurd:
  46 contradiction:
  47 exact:
  48 elim_type:
  49 fourier:
  50 ring:
  51
  52 ####
  53 applyP:
  54 fwd_simpl: