prop_logic : THEORY
  BEGIN
    A, B, C, D: bool
    ex1: LEMMA A IMPLIES (B OR A)
    ex2: LEMMA (A AND (A IMPLIES B)) IMPLIES B
    ex3: LEMMA ((A IMPLIES B) IMPLIES A) IMPLIES (B IMPLIES (B AND A))
  END prop_logic