ConseqConv.GEN

When applied to a term x and a theorem [A1, A2] |- t, where x occurs in A1 but not in A2, the inference rule GEN_ASSUM returns the theorem [!x. A1 x, A2 |- !x. t. There is no compulsion that x should be free in t.

GEN_ASSUM is a generalisation of GEN. While GEN fails, if x is free in an assumption, GEN_ASSUM succeeds.

        A1, A2 |- t
   ---------------------    GEN_ASSUM x   [where x is free in A1, but not in A2]
   (!x. A1), A2 |- !x. t