diff --git a/src/Proof.idr b/src/Proof.idr
index ab0af7f..adbac77 100644
--- a/src/Proof.idr
+++ b/src/Proof.idr
@@ -22,4 +22,4 @@ data Proof : Context sig g -> Formula sig n -> Type where
   ImpE    : Proof c (Imp phi psi) -> Proof c phi -> Proof c psi
   ForallI : Proof c phi -> Proof c (Forall phi)
   ForallE : Proof c (Forall phi) -> Proof c (elimBinder t phi)
-  Weaken  : Proof c1 phi -> Subset c1 c2 -> Proof c2 phi
+  Weaken  : Proof c1 phi -> Subset c1 c2 => Proof c2 phi
diff --git a/src/Test.idr b/src/Test.idr
index 9012163..01b3e56 100644
--- a/src/Test.idr
+++ b/src/Test.idr
@@ -113,7 +113,7 @@ doubleNeg :
   Proof c (Not (Not phi)) -> Proof c phi
 doubleNeg pf =
   Contra $
-  ImpE (Weaken pf (Missing Same)) $
+  ImpE (Weaken pf) $
   Hyp 0
   
 AndI : {d : _} -> {c : _} ->
@@ -124,5 +124,5 @@ AndI pfPhi pfPsi =
   ImpI $
   ImpE
     (ImpE (Hyp 0) $
-     Weaken pfPhi $ Missing Same)
-    (Weaken pfPsi $ Missing Same)
+     Weaken pfPhi)
+    (Weaken pfPsi)