_⇒_ : Bool → Bool → Bool
false  ⇒  _ = true
true  ⇒  true = true
true  ⇒  false = false

Axiom : Cond -> PrimComm -> Cond -> Set
Axiom pre comm post = ∀ (env : Env) →  (pre env) ⇒ ( post (comm env)) ≡ true

Tautology : Cond -> Cond -> Set
Tautology pre post = ∀ (env : Env) →  (pre env)  ⇒ (post env) ≡ true