Using the tactic "dependent induction" inside a match goal seems not to work.

gistfile1.txt

subtype_weaken_l < Show.
1 subgoal
  
  C : constraints
  AT : annotatedtype
  AT' : annotatedtype
  H : subtype C AT AT'
  ============================
   forall C' : list ineq, subtype (C ++ C') AT AT'

subtype_weaken_l < (match goal with
subtype_weaken_l <  | H : subtype _ _ _ |- _ => induction H
subtype_weaken_l <  end).
4 subgoals
  
  C : constraints
  AT : annotatedtype
  ============================
   forall C' : list ineq, subtype (C ++ C') AT AT

subgoal 2 is:
 forall C' : list ineq, subtype (C ++ C') AT_1 AT_3
subgoal 3 is:
 forall C' : list ineq, subtype (C ++ C') (at_Lock r_1) (at_Lock r_2)
subgoal 4 is:
 forall C' : list ineq,
 subtype (C ++ C') (at_Arrow AT_1 (EffectIntro D_1 D_2) AT_2)
   (at_Arrow AT_1' (EffectIntro D_1' D_2') AT_2')

subtype_weaken_l < Undo.
1 subgoal
  
  C : constraints
  AT : annotatedtype
  AT' : annotatedtype
  H : subtype C AT AT'
  ============================
   forall C' : list ineq, subtype (C ++ C') AT AT'

subtype_weaken_l < (match goal with
subtype_weaken_l <  | H : subtype _ _ _ |- _ => dependent induction H
subtype_weaken_l <  end).
Error: No matching clauses for match goal
       (use "Set Ltac Debug" for more info).