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