--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/axiom-taut.agda.replaced	Sun Apr 24 23:13:44 2022 +0900
@@ -0,0 +1,10 @@
+_!$\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