some progress with logic

[juan_gandhi]

for { p <- Ω.points } {
  val pp = predicateFor(p)
  (True ∧ pp) === pp
  (False ∧ pp) === False

  // idempotence
  (pp ∧ pp) === pp

  for { q <- Ω.points } {
    val pq = predicateFor(q)
    val ppq = pp ∧ pq
    
    // commutativity
    (pp ∧ pq) === (pq ∧ pp)
    
    for { r <- Ω.points } {
      val pr = predicateFor(r)
      // associativity
      (ppq ∧ pr) === (pp ∧ (pq ∧ pr))
    }
  }
}