// ========
// Proof of associativity of "or":
// ========

// === Declarations: ===
LET A î BOOL
LET B î BOOL
LET C î BOOL

// === Main goal: ===
// (The proof is restricted to one side of the equivalence to keep the
// proof short)
GOAL (NOVARS) A or (B or C) => (A or B) or C