diff --git a/wp.v b/wp.v
index ec3360c..cd25bdb 100644
--- a/wp.v
+++ b/wp.v
@@ -163,41 +163,39 @@ Definition assertImplLogical : Assert -> Assert -> Prop :=
 
 (***** Hoare provability *****************************************************)
 
-Parameter  hoare_provability : Assert -> Instr -> Assert -> Prop.
-Notation "|- [| pre  |] instr  [| post |]" :=
-        (hoare_provability pre instr post) (at level 30): assert.
+Reserved Notation "|- [| x |] y [| z |]" (at level 30).
 
-Axiom h_skip: forall (asser: Assert), ( |- [|asser|] skip [|asser|]) % assert.
-Axiom h_abort: forall (a1:Assert), forall (a2: Assert),
-    (|- [|a1|] abort [|a2|]) % assert.
-Axiom h_assign: forall (asser: Assert), forall (x: Var), forall (e: Expr),
-    (|- [| asser [[ x <- expr e ]] |] (assign x e) [|asser|]) % assert.
-Axiom h_conseq:
-    forall (a1: Assert), forall (a1': Assert),
-    forall (a2: Assert), forall (a2': Assert),
-    forall (s: Instr),
-    (|- [| a1' |] s [| a2' |]) % assert ->
-            (assertImplLogical a1 a1') ->
-            (assertImplLogical a2' a2) ->
-            (|- [| a1 |] s [| a2 |]) % assert.
-Axiom h_seq:
-    forall (a1: Assert), forall (a2: Assert), forall (a3: Assert),
-    forall (s1: Instr), forall (s2: Instr),
-    (|- [|a1|] s1 [|a2|]) % assert -> (|- [|a2|] s2 [|a3|]) % assert ->
-            (|- [|a1|] (seq s1 s2) [|a3|]) % assert.
-Axiom h_if:
-    forall (a1: Assert), forall (a2: Assert),
-    forall (e: Expr),
-    forall (s1: Instr), forall (s2: Instr),
-    (|- [| a1 /\ (assertOfExpr e) |] s1 [| a2 |]) % assert ->
-        (|- [| a1 /\ ~ (assertOfExpr e) |] s2 [| a2 |]) % assert ->
-        (|- [| a1 |] (ifelse e s1 s2) [| a2 |]) % assert.
-Axiom h_while:
-    forall (inv: Assert),
-    forall (e: Expr),
-    forall (s: Instr),
-    (|- [| inv /\ (assertOfExpr e) |] s [| inv |]) % assert ->
-        (|- [| inv |] (while e s) [| inv /\ ~ (assertOfExpr e) |]) % assert.
+Inductive hoare_provability : Assert -> Instr -> Assert -> Prop :=
+    | H_skip: forall pre, hoare_provability pre skip pre
+    | H_abort: forall pre, forall post, hoare_provability pre abort post
+    | H_assign: forall post, forall (x: Var), forall (e: Expr),
+        (|- [| post [[ x <- expr e ]] |] (assign x e) [| post |]) % assert
+    | H_conseq:
+        forall pre, forall post,
+        forall pre', forall post',
+        forall s,
+
+        (|- [| pre' |] s [| post' |]) % assert ->
+            (assertImplLogical pre pre') ->
+            (assertImplLogical post' post) ->
+            (|- [| pre |] s [| post |]) % assert
+    | H_seq:
+        forall pre, forall mid, forall post, forall s1, forall s2,
+        (|- [|pre|] s1 [|mid|]) % assert ->
+            (|- [|mid|] s2 [|post|]) % assert ->
+            (|- [|pre|] (seq s1 s2) [|post|]) % assert
+    | H_if:
+        forall pre, forall post, forall expr, forall sIf, forall sElse,
+        (|- [| pre /\ (assertOfExpr expr) |] sIf [| post |]) % assert ->
+            (|- [| pre /\ ~(assertOfExpr expr) |] sElse [| post |]) % assert ->
+            (|- [| pre |] (ifelse expr sIf sElse) [| post |]) % assert
+    | H_while:
+        forall inv, forall expr, forall sBody,
+        (|- [| inv /\ (assertOfExpr expr) |] sBody [| inv |]) % assert ->
+            (|- [| inv |] (while expr sBody)
+                    [| inv /\ ~ (assertOfExpr expr) |]) % assert
+where "|- [| pre  |] instr  [| post |]" :=
+        (hoare_provability pre instr post) : assert.
 
 (***** Hoare: provability implies consequence ********************************)