_@$\Rightarrow$@_ : Bool → Bool → Bool
false  @$\Rightarrow$@  _ = true
true  @$\Rightarrow$@  true = true
true  @$\Rightarrow$@  false = false

Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set
Axiom pre comm post = ∀ (env : Env) →  (pre env) @$\Rightarrow$@ ( post (comm env)) @$\equiv$@ true

Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set
Tautology pre post = ∀ (env : Env) →  (pre env)  @$\Rightarrow$@ (post env) @$\equiv$@ true