//  DEMO1:

// Let A and B be propositions:
LET A î BOOL
LET B î BOOL

// Prove commutativity of conjunctions:
GOAL (NOVARS) A & B => B & A