--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/axiom-taut.agda.replaced	Tue Sep 08 18:38:08 2020 +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