Inductive prodTactic (A : Type) (B : Type) : Type := pairTactic : A → B → prodTactic A B.
Implicit Arguments pairTactic [A B].
Inductive unitTactic : Type := ttTactic : unitTactic.

Notation "[ x , y , .. , z ]" := (pairTactic .. (pairTactic x y) .. z) (at level 1) : tactic_scope.

Open Scope tactic_scope.

Ltac taclistFwd tac l :=
match type of l with
|(prodTactic _ _) ⇒
 match l with
 |(pairTactic ?y ?a) ⇒ taclistFwd tac y; taclistFwd tac a
 end
|_⇒tac l
end.

Ltac taclistRev tac l :=
match type of l with
|(prodTactic _ _) ⇒
 match l with
 |(pairTactic ?y ?a) ⇒ taclistRev tac a; taclistRev tac y
 end
|_⇒tac l
end.

Ltac discharge x :=
 let dischargeOne a := generalize a; clear a in
  taclistRev dischargeOne x.

Ltac gen expr lst :=
match type of lst with
|(prodTactic _ _) ⇒
 match lst with
 |(pairTactic ?p ?q) ⇒ let first := gen expr q in gen first p
 end
|_ ⇒
  match (eval pattern lst in expr) with
    (?f ?z) ⇒
     let Z := type of lst
     in constr:(∀ n:Z, f n)
  end
end.

Ltac introNames :=
match goal with
H : unitTactic |- _ ⇒ clear H; intro H; introNames
|_ ⇒ idtac
end.

Ltac wlog nn expr lst :=
match goal with
| |- ?g ⇒
 let full := gen (expr → g) lst in
 cut full;
 [intro | let c x := clear x; pose (x:=ttTactic) in taclistRev c lst; introNames; intro nn]
end.