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

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

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