Ldi_rules = Ldi_rules_nd + Uc + WkDel + consts ldi_rules_a :: "(structr sequent list * structr sequent) set" inductive "ldi_rules_a" intrs na "r : ldi_rules ==> r : ldi_rules_a" assoc "r : rulefs {assoc} ==> r : ldi_rules_a" end